A2: dom f = the carrier of U1 by FUNCT_2:def 1;
then reconsider A = f .: the carrier of U1 as non empty Subset of U2 by RELAT_1:152;
take B = UniAlgSetClosed A; :: thesis: the carrier of B = f .: the carrier of U1
A is opers_closed

proof

let o2 be operation of U2; :: according to UNIALG_2:def 5 :: thesis: A is_closed_on o2
consider n being Nat such that
A3: ( n in dom the charact of U2 & the charact of U2 . n = o2 ) by FINSEQ_2:11;
A4: U1,U2 are_similar by A1, Def1;
then A5: signature U1 = signature U2 by UNIALG_2:def 2;
A6: ( len (signature U1) = len the charact of U1 & len (signature U2) = len the charact of U2 ) by UNIALG_1:def 11;
A7: ( dom the charact of U1 = Seg (len the charact of U1) & dom the charact of U2 = Seg (len the charact of U2) & dom (signature U1) = Seg (len (signature U1)) & dom (signature U1) = dom (signature U2) & dom (signature U2) = Seg (len (signature U2)) ) by A4, FINSEQ_1:def 3, UNIALG_2:def 2;
then reconsider o1 = the charact of U1 . n as operation of U1 by A3, A6, FUNCT_1:def 5;
let s be FinSequence of A; :: according to UNIALG_2:def 4 :: thesis: ( not len s = arity o2 or o2 . s in A )
assume A8: len s = arity o2 ; :: thesis: o2 . s in A
A9: ( (signature U1) . n = arity o1 & (signature U2) . n = arity o2 ) by A3, A6, A7, UNIALG_1:def 11;
defpred S₁[ set , set ] means f . $2 = s . $1;
A10: for x being set st x in dom s holds
ex y being set st
( y in the carrier of U1 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in dom s implies ex y being set st
( y in the carrier of U1 & S₁[x,y] ) )
assume A11: x in dom s ; :: thesis: ex y being set st
( y in the carrier of U1 & S₁[x,y] )
then reconsider x0 = x as Element of NAT ;
s . x0 in A by A11, FINSEQ_2:13;
then consider y being set such that
A12: ( y in dom f & y in the carrier of U1 & f . y = s . x0 ) by FUNCT_1:def 12;
take y ; :: thesis: ( y in the carrier of U1 & S₁[x,y] )
thus ( y in the carrier of U1 & S₁[x,y] ) by A12; :: thesis: verum

end;

consider s1 being Function such that
A13: ( dom s1 = dom s & rng s1 c= the carrier of U1 & ( for x being set st x in dom s holds
S₁[x,s1 . x] ) ) from WELLORD2:sch 1(A10);
dom s1 = Seg (len s) by A13, FINSEQ_1:def 3;
then reconsider s1 = s1 as FinSequence by FINSEQ_1:def 2;
reconsider s1 = s1 as FinSequence of U1 by A13, FINSEQ_1:def 4;
reconsider s1 = s1 as Element of the carrier of U1 * by FINSEQ_1:def 11;
A14: len s1 = len s by A13, FINSEQ_3:31;
then s1 in { w where w is Element of the carrier of U1 * : len w = arity o1 } by A5, A8, A9;
then s1 in (arity o1) -tuples_on the carrier of U1 by FINSEQ_2:def 4;
then A15: s1 in dom o1 by UNIALG_2:2;
then A16: f . (o1 . s1) = o2 . (f * s1) by A1, A3, A6, A7, Def1;
A17: len (f * s1) = len s1 by Th1;
A18: dom (f * s1) = Seg (len (f * s1)) by FINSEQ_1:def 3;
X: dom s = Seg (len s1) by A13, FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom s implies (f * s1) . m = s . m )
assume A19: m in dom s ; :: thesis: (f * s1) . m = s . m
then f . (s1 . m) = s . m by A13;
hence (f * s1) . m = s . m by A17, A18, A19, Th1, X; :: thesis: verum

end;

then A20: s = f * s1 by A14, A17, FINSEQ_2:10;
( rng o1 c= the carrier of U1 & o1 . s1 in rng o1 ) by A15, FUNCT_1:def 5;
hence o2 . s in A by A2, A16, A20, FUNCT_1:def 12; :: thesis: verum

end;

then B = UAStr(# A,(Opers U2,A) #) by UNIALG_2:def 9;
hence the carrier of B = f .: the carrier of U1 ; :: thesis: verum