defpred S₁[ set , set ] means f . $1 = f . $2;
set u1 = the carrier of U1;
consider R being Relation of the carrier of U1, the carrier of U1 such that
A2: for x, y being Element of the carrier of U1 holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
R is_reflexive_in the carrier of U1

proof

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in the carrier of U1 or [x,x] in R )
assume x in the carrier of U1 ; :: thesis: [x,x] in R
then reconsider x1 = x as Element of the carrier of U1 ;
f . x1 = f . x1 ;
hence [x,x] in R by A2; :: thesis: verum

end;

then A3: ( dom R = the carrier of U1 & field R = the carrier of U1 ) by ORDERS_1:13;
A4: R is_transitive_in the carrier of U1

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of U1 or not y in the carrier of U1 or not z in the carrier of U1 or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume that
A5: ( x in the carrier of U1 & y in the carrier of U1 & z in the carrier of U1 ) and
A6: ( [x,y] in R & [y,z] in R ) ; :: thesis: [x,z] in R
reconsider x1 = x, y1 = y, z1 = z as Element of the carrier of U1 by A5;
( f . x1 = f . y1 & f . y1 = f . z1 ) by A2, A6;
hence [x,z] in R by A2; :: thesis: verum

end;

R is_symmetric_in the carrier of U1

proof

let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in the carrier of U1 or not y in the carrier of U1 or not [x,y] in R or [y,x] in R )
assume that
A7: ( x in the carrier of U1 & y in the carrier of U1 ) and
A8: [x,y] in R ; :: thesis: [y,x] in R
reconsider x1 = x, y1 = y as Element of the carrier of U1 by A7;
f . x1 = f . y1 by A2, A8;
hence [y,x] in R by A2; :: thesis: verum

end;

then reconsider R = R as Equivalence_Relation of U1 by A3, A4, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

now :: thesis: for n being Nat
for o being operation of U1 st n in dom the charact of U1 & o = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R

U1,U2 are_similar by A1;
then A9: signature U1 = signature U2 ;
let n be Nat; :: thesis: for o being operation of U1 st n in dom the charact of U1 & o = the charact of U1 . n holds
for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R
let o be operation of U1; :: thesis: ( n in dom the charact of U1 & o = the charact of U1 . n implies for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R )
assume that
A10: n in dom the charact of U1 and
A11: o = the charact of U1 . n ; :: thesis: for x, y being FinSequence of U1 st x in dom o & y in dom o & [x,y] in ExtendRel R holds
[(o . x),(o . y)] in R
( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def 4;
then dom the charact of U2 = dom the charact of U1 by A9, FINSEQ_3:29;
then reconsider o2 = the charact of U2 . n as operation of U2 by A10, FUNCT_1:def 3;
let x, y be FinSequence of U1; :: thesis: ( x in dom o & y in dom o & [x,y] in ExtendRel R implies [(o . x),(o . y)] in R )
assume that
A12: ( x in dom o & y in dom o ) and
A13: [x,y] in ExtendRel R ; :: thesis: [(o . x),(o . y)] in R
( o . x in rng o & o . y in rng o ) by A12, FUNCT_1:def 3;
then reconsider ox = o . x, oy = o . y as Element of the carrier of U1 ;
A14: len x = len y by A13, FINSEQ_3:def 3;
A15: len (f * y) = len y by FINSEQ_3:120;
then A16: dom (f * y) = Seg (len x) by A14, FINSEQ_1:def 3;
A17: len (f * x) = len x by FINSEQ_3:120;

A18: now :: thesis: for m being Nat st m in dom (f * y) holds
(f * y) . m = (f * x) . m

let m be Nat; :: thesis: ( m in dom (f * y) implies (f * y) . m = (f * x) . m )
assume A19: m in dom (f * y) ; :: thesis: (f * y) . m = (f * x) . m
then m in dom y by A14, A16, FINSEQ_1:def 3;
then A20: y . m in rng y by FUNCT_1:def 3;
A21: m in dom x by A16, A19, FINSEQ_1:def 3;
then x . m in rng x by FUNCT_1:def 3;
then reconsider xm = x . m, ym = y . m as Element of the carrier of U1 by A20;
[(x . m),(y . m)] in R by A13, A21, FINSEQ_3:def 3;
then A22: f . xm = f . ym by A2
.= (f * y) . m by A19, FINSEQ_3:120 ;
m in dom (f * x) by A17, A16, A19, FINSEQ_1:def 3;
hence (f * y) . m = (f * x) . m by A22, FINSEQ_3:120; :: thesis: verum

end;

( f . (o . x) = o2 . (f * x) & f . (o . y) = o2 . (f * y) ) by A1, A10, A11, A12;
then f . ox = f . oy by A14, A17, A15, A18, FINSEQ_2:9;
hence [(o . x),(o . y)] in R by A2; :: thesis: verum

end;

then reconsider R = R as Congruence of U1 by Def7;
take R ; :: thesis: for a, b being Element of U1 holds
( [a,b] in R iff f . a = f . b )
let a, b be Element of the carrier of U1; :: thesis: ( [a,b] in R iff f . a = f . b )
thus ( [a,b] in R implies f . a = f . b ) by A2; :: thesis: ( f . a = f . b implies [a,b] in R )
assume f . a = f . b ; :: thesis: [a,b] in R
hence [a,b] in R by A2; :: thesis: verum