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 ;
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 4 :: thesis: A is_closed_on o2
consider n being Nat such that
A3: n in dom the charact of U2 and
A4: the charact of U2 . n = o2 by FINSEQ_2:10;
let s be FinSequence of A; :: according to UNIALG_2:def 3 :: thesis: ( not len s = arity o2 or o2 . s in A )
assume A5: len s = arity o2 ; :: thesis: o2 . s in A
defpred S₁[ set , set ] means f . $2 = s . $1;
A6: 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 A7: 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 A7, FINSEQ_2:11;
then consider y being set such that
A8: y in dom f and
y in the carrier of U1 and
A9: f . y = s . x0 by FUNCT_1:def 6;
take y ; :: thesis: ( y in the carrier of U1 & S₁[x,y] )
thus ( y in the carrier of U1 & S₁[x,y] ) by A8, A9; :: thesis: verum

end;

consider s1 being Function such that
A10: ( 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 FUNCT_1:sch 5(A6);
dom s1 = Seg (len s) by A10, FINSEQ_1:def 3;
then reconsider s1 = s1 as FinSequence by FINSEQ_1:def 2;
reconsider s1 = s1 as FinSequence of U1 by A10, FINSEQ_1:def 4;
reconsider s1 = s1 as Element of the carrier of U1 * by FINSEQ_1:def 11;
A11: len s1 = len s by A10, FINSEQ_3:29;
A12: dom (signature U2) = Seg (len (signature U2)) by FINSEQ_1:def 3;
A13: U1,U2 are_similar by A1, Def1;
then A14: signature U1 = signature U2 by UNIALG_2:def 1;
A15: dom (signature U1) = dom (signature U2) by A13, UNIALG_2:def 1;
A16: ( len (signature U2) = len the charact of U2 & dom the charact of U2 = Seg (len the charact of U2) ) by FINSEQ_1:def 3, UNIALG_1:def 4;
then A17: (signature U2) . n = arity o2 by A3, A4, A12, UNIALG_1:def 4;
A18: len (f * s1) = len s1 by FINSEQ_3:120;
A19: ( dom (f * s1) = Seg (len (f * s1)) & dom s = Seg (len s1) ) by A10, FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom s implies (f * s1) . m = s . m )
assume A20: m in dom s ; :: thesis: (f * s1) . m = s . m
then f . (s1 . m) = s . m by A10;
hence (f * s1) . m = s . m by A18, A19, A20, FINSEQ_3:120; :: thesis: verum

end;

then A21: s = f * s1 by A11, A18, FINSEQ_2:9;
A22: dom (signature U1) = Seg (len (signature U1)) by FINSEQ_1:def 3;
A23: ( len (signature U1) = len the charact of U1 & dom the charact of U1 = Seg (len the charact of U1) ) by FINSEQ_1:def 3, UNIALG_1:def 4;
then reconsider o1 = the charact of U1 . n as operation of U1 by A3, A16, A22, A15, A12, FUNCT_1:def 3;
(signature U1) . n = arity o1 by A3, A16, A15, A12, UNIALG_1:def 4;
then s1 in { w where w is Element of the carrier of U1 * : len w = arity o1 } by A14, A5, A17, A11;
then s1 in (arity o1) -tuples_on the carrier of U1 by FINSEQ_2:def 4;
then A24: s1 in dom o1 by MARGREL1:22;
then A25: o1 . s1 in rng o1 by FUNCT_1:def 3;
f . (o1 . s1) = o2 . (f * s1) by A1, A3, A4, A23, A16, A22, A15, A12, A24, Def1;
hence o2 . s in A by A2, A21, A25, FUNCT_1:def 6; :: thesis: verum

end;

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