defpred S₁[ set ] means ( A c= $1 & Constants U0 c= $1 & ( for B being non empty Subset of U0 st B = $1 holds
B is opers_closed ) );
set C = bool the carrier of U0;
consider X being set such that
A2: for x being set holds
( x in X iff ( x in bool the carrier of U0 & S₁[x] ) ) from XFAMILY:sch 1();
set P = meet X;
( the carrier of U0 in bool the carrier of U0 & ( for B being non empty Subset of U0 st B = the carrier of U0 holds
B is opers_closed ) ) by Th4, ZFMISC_1:def 1;
then A3: the carrier of U0 in X by A2;
A4: meet X c= the carrier of U0 by A3, SETFAM_1:def 1;

end;

let o be operation of U0; :: according to UNIALG_2:def 4 :: thesis:
let s be FinSequence of P; :: according to UNIALG_2:def 3 :: thesis:
assume A7: len s = arity o ; :: thesis:

let a be set ; :: thesis:
A8: rng s c= P by FINSEQ_1:def 4;
assume A9: a in X ; :: thesis:
then reconsider a0 = a as Subset of U0 by A2;
( A c= a0 & Constants U0 c= a0 ) by A2, A9;
then reconsider a0 = a0 as non empty Subset of U0 by A1;
P c= a0 by A9, SETFAM_1:3;
then rng s c= a0 by A8;
then reconsider s0 = s as FinSequence of a0 by FINSEQ_1:def 4;
a0 is opers_closed by A2, A9;
then a0 is_closed_on o ;
then o . s0 in a0 by A7;
hence o . s in a ; :: thesis:

end;

end;

then A10: E = UAStr(# P,(Opers (U0,P)) #) by Def8;
A c= A \/ (Constants U0) by XBOOLE_1:7;
hence A c= the carrier of E by A5, A10; :: thesis:
let U1 be SubAlgebra of U0; :: thesis:
assume A11: A c= the carrier of U1 ; :: thesis:
set u1 = the carrier of U1;
A12: Constants U0 c= the carrier of U1

reconsider B = the carrier of U1 as non empty Subset of U0 by Def7;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Constants U0 ; :: thesis:
then consider a being Element of U0 such that
A13: a = x and
A14: ex o being operation of U0 st
( arity o = 0 & a in rng o ) ;
consider o0 being operation of U0 such that
A15: arity o0 = 0 and
A16: a in rng o0 by A14;
consider y being object such that
A17: y in dom o0 and
A18: a = o0 . y by A16, FUNCT_1:def 3;
dom o0 = 0 -tuples_on the carrier of U0 by A15, MARGREL1:22
.= {(<*> the carrier of U0)} by FINSEQ_2:94 ;
then y in {(<*> B)} by A17;
then y in 0 -tuples_on B by FINSEQ_2:94;
then y in (dom o0) /\ ((arity o0) -tuples_on B) by A15, A17, XBOOLE_0:def 4;
then A19: y in dom (o0 | ((arity o0) -tuples_on B)) by RELAT_1:61;
consider n being Nat such that
A20: n in dom the charact of U0 and
A21: the charact of U0 . n = o0 by FINSEQ_2:10;
A22: n in dom the charact of U1 by A20, Th7;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def 3;
the charact of U1 = Opers (U0,B) by Def7;
then A23: o1 = o0 /. B by A21, A22, Def6;
B is opers_closed by Def7;
then A24: B is_closed_on o0 ;
then y in dom (o0 /. B) by A19, Def5;
then A25: o1 . y in rng o1 by A23, FUNCT_1:def 3;
A26: rng o1 c= the carrier of U1 by RELAT_1:def 19;
o1 . y = (o0 | ((arity o0) -tuples_on B)) . y by A23, A24, Def5
.= a by A18, A19, FUNCT_1:47 ;
hence x in the carrier of U1 by A13, A25, A26; :: thesis:

end;

( the carrier of U1 is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of U1 holds
B is opers_closed ) ) by Def7;
then A27: the carrier of U1 in X by A2, A11, A12;
hence the carrier of E is Subset of U1 by A10, SETFAM_1:3; :: according to UNIALG_2:def 7 :: thesis:
let B be non empty Subset of U1; :: thesis:
assume A28: B = the carrier of E ; :: thesis:
reconsider u11 = the carrier of U1 as non empty Subset of U0 by Def7;
A29: the charact of U1 = Opers (U0,u11) by Def7;
A30: dom the charact of U0 = dom (Opers (U0,u11)) by Def6;
A31: u11 is opers_closed by Def7;

let o1 be operation of U1; :: thesis:
consider n being Nat such that
A33: n in dom the charact of U1 and
A34: o1 = the charact of U1 . n by FINSEQ_2:10;
reconsider o0 = the charact of U0 . n as operation of U0 by A29, A30, A33, FUNCT_1:def 3;
A35: arity o0 = arity o1 by A33, A34, Th6;
A36: u11 is_closed_on o0 by A31;

let s be FinSequence of B; :: thesis:
A37: P is_closed_on o0 by A6;
reconsider sE = s as Element of P * by A10, A28, FINSEQ_1:def 11;
s is FinSequence of u11 by FINSEQ_2:24;
then reconsider s1 = s as Element of u11 * by FINSEQ_1:def 11;
A38: dom (o0 | ((arity o0) -tuples_on u11)) = (dom o0) /\ ((arity o0) -tuples_on u11) by RELAT_1:61
.= ((arity o0) -tuples_on the carrier of U0) /\ ((arity o0) -tuples_on u11) by MARGREL1:22
.= (arity o0) -tuples_on u11 by MARGREL1:21 ;
assume A39: len s = arity o1 ; :: thesis:
then s1 in { q where q is Element of u11 * : len q = arity o0 } by A35;
then A40: s1 in dom (o0 | ((arity o0) -tuples_on u11)) by A38, FINSEQ_2:def 4;
o1 . s = (o0 /. u11) . s1 by A29, A33, A34, Def6
.= (o0 | ((arity o0) -tuples_on u11)) . s1 by A36, Def5
.= o0 . sE by A40, FUNCT_1:47 ;
hence o1 . s in B by A10, A28, A35, A39, A37; :: thesis:

end;

end;

A41: dom (Opers (U1,B)) = dom the charact of U1 by Def6;
A42: dom the charact of U0 = dom (Opers (U0,P)) by Def6;
A43: P c= the carrier of U1 by A27, SETFAM_1:3;

let n be Nat; :: thesis:
assume A44: n in dom the charact of U0 ; :: thesis:
then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;
reconsider o1 = the charact of U1 . n as operation of U1 by A29, A30, A44, FUNCT_1:def 3;
A45: u11 is_closed_on o0 by A31;
A46: P is_closed_on o0 by A6;
thus the charact of E . n = o0 /. P by A10, A42, A44, Def6
.= o0 | ((arity o0) -tuples_on P) by A46, Def5
.= o0 | (((arity o0) -tuples_on u11) /\ ((arity o0) -tuples_on P)) by A43, MARGREL1:21
.= (o0 | ((arity o0) -tuples_on u11)) | ((arity o0) -tuples_on P) by RELAT_1:71
.= (o0 /. u11) | ((arity o0) -tuples_on P) by A45, Def5
.= o1 | ((arity o0) -tuples_on P) by A29, A30, A44, Def6
.= o1 | ((arity o1) -tuples_on B) by A10, A28, A29, A30, A44, Th6
.= o1 /. B by A32, Def5
.= (Opers (U1,B)) . n by A29, A30, A41, A44, Def6 ; :: thesis:

end;