let U0 be Universal_Algebra; :: thesis: for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds
U1 is SubAlgebra of U2

let U1, U2 be SubAlgebra of U0; :: thesis: ( the carrier of U1 c= the carrier of U2 implies U1 is SubAlgebra of U2 )
A1: dom the charact of U1 = dom the charact of U0 by Th7;
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;
assume A2: the carrier of U1 c= the carrier of U2 ; :: thesis: U1 is SubAlgebra of U2
hence the carrier of U1 is Subset of U2 ; :: according to UNIALG_2:def 7 :: thesis: for B being non empty Subset of U2 st B = the carrier of U1 holds
( the charact of U1 = Opers (U2,B) & B is opers_closed )

let B be non empty Subset of U2; :: thesis: ( B = the carrier of U1 implies ( the charact of U1 = Opers (U2,B) & B is opers_closed ) )
assume A3: B = the carrier of U1 ; :: thesis: ( the charact of U1 = Opers (U2,B) & B is opers_closed )
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;
A4: the charact of U2 = Opers (U0,B2) by Def7;
A5: B2 is opers_closed by Def7;
A6: dom (Opers (U2,B)) = dom the charact of U2 by Def6;
A7: dom the charact of U2 = dom the charact of U0 by Th7;
A8: B1 is opers_closed by Def7;
A9: B is opers_closed
proof
let o2 be operation of U2; :: according to UNIALG_2:def 4 :: thesis: B is_closed_on o2
let s be FinSequence of B; :: according to UNIALG_2:def 3 :: thesis: ( len s = arity o2 implies o2 . s in B )
consider n being Nat such that
A10: n in dom the charact of U2 and
A11: the charact of U2 . n = o2 by FINSEQ_2:10;
reconsider o0 = the charact of U0 . n as operation of U0 by ;
A12: arity o2 = arity o0 by ;
rng s c= B by FINSEQ_1:def 4;
then rng s c= B2 by XBOOLE_1:1;
then s is FinSequence of B2 by FINSEQ_1:def 4;
then reconsider s2 = s as Element of B2 * by FINSEQ_1:def 11;
reconsider s1 = s as Element of B1 * by ;
assume A13: arity o2 = len s ; :: thesis: o2 . s in B
set tb2 = (arity o0) -tuples_on B2;
A14: B2 is_closed_on o0 by A5;
A15: o2 = o0 /. B2 by A4, A10, A11, Def6
.= o0 | ((arity o0) -tuples_on B2) by ;
A16: B1 is_closed_on o0 by A8;
(arity o0) -tuples_on B2 = { w where w is Element of B2 * : len w = arity o0 } by FINSEQ_2:def 4;
then s2 in (arity o0) -tuples_on B2 by ;
then o2 . s = o0 . s1 by ;
hence o2 . s in B by A3, A13, A16, A12; :: thesis: verum
end;
A17: the charact of U1 = Opers (U0,B1) by Def7;
now :: thesis: for n being Nat st n in dom the charact of U0 holds
the charact of U1 . n = (Opers (U2,B)) . n
let n be Nat; :: thesis: ( n in dom the charact of U0 implies the charact of U1 . n = (Opers (U2,B)) . n )
assume A18: n in dom the charact of U0 ; :: thesis: the charact of U1 . n = (Opers (U2,B)) . n
then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;
reconsider o2 = the charact of U2 . n as operation of U2 by ;
A19: ( o2 = o0 /. B2 & arity o2 = arity o0 ) by A4, A7, A18, Def6, Th6;
A20: B is_closed_on o2 by A9;
A21: B2 is_closed_on o0 by A5;
A22: B1 is_closed_on o0 by A8;
thus the charact of U1 . n = o0 /. B1 by A17, A1, A18, Def6
.= o0 | ((arity o0) -tuples_on B1) by
.= o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1)) by
.= (o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B) by
.= (o0 /. B2) | ((arity o0) -tuples_on B) by
.= o2 /. B by
.= (Opers (U2,B)) . n by A7, A6, A18, Def6 ; :: thesis: verum
end;
hence the charact of U1 = Opers (U2,B) by ; :: thesis: B is opers_closed
thus B is opers_closed by A9; :: thesis: verum