Theorem resseuf

Description: The Euclidean function is unaffected by structure restriction. (Contributed by Thierry Arnoux, 9-Nov-2026)

	Ref	Expression
Hypotheses	resseuf.h	|- H = ( G |`s A )
	resseuf.f	|- F = ( EuclF ` G )
Assertion	resseuf	|- ( A e. V -> F = ( EuclF ` H ) )

Proof

Step	Hyp	Ref	Expression
1		resseuf.h	|- H = ( G |`s A )
2		resseuf.f	|- F = ( EuclF ` G )
3		eufid	|- EuclF = Slot ( EuclF ` ndx )
4		basendxneufndx	|- ( Base ` ndx ) =/= ( EuclF ` ndx )
5	4	necomi	|- ( EuclF ` ndx ) =/= ( Base ` ndx )
6	1 2 3 5	resseqnbas	|- ( A e. V -> F = ( EuclF ` H ) )