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 )
assume A1:
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 8 :: 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 )
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def8;
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def8;
A2:
( the charact of U1 = Opers U0,B1 & B1 is opers_closed & the charact of U2 = Opers U0,B2 & B2 is opers_closed )
by Def8;
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 )
A4:
( dom the charact of U1 = dom the charact of U0 & dom the charact of U2 = dom the charact of U0 & dom (Opers U0,B1) = dom the charact of U0 & dom (Opers U0,B2) = dom the charact of U0 & dom (Opers U2,B) = dom the charact of U2 )
by Def7, Th10;
A5:
B is opers_closed
proof
let o2 be
operation of
U2;
:: according to UNIALG_2:def 5 :: thesis: B is_closed_on o2let s be
FinSequence of
B;
:: according to UNIALG_2:def 4 :: thesis: ( len s = arity o2 implies o2 . s in B )
assume A6:
arity o2 = len s
;
:: thesis: o2 . s in B
(
B c= B2 &
rng s c= B )
by FINSEQ_1:def 4;
then A7:
(
rng s c= B2 &
B2 c= the
carrier of
U0 )
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 A3, FINSEQ_1:def 11;
rng s c= the
carrier of
U0
by A7, XBOOLE_1:1;
then
s is
FinSequence of the
carrier of
U0
by FINSEQ_1:def 4;
then reconsider s0 =
s as
Element of the
carrier of
U0 * by FINSEQ_1:def 11;
consider n being
Nat such that A8:
(
n in dom the
charact of
U2 & the
charact of
U2 . n = o2 )
by FINSEQ_2:11;
reconsider o0 = the
charact of
U0 . n as
operation of
U0 by A4, A8, FUNCT_1:def 5;
set tb2 =
(arity o0) -tuples_on B2;
set tb0 =
(arity o0) -tuples_on the
carrier of
U0;
A9:
(
(arity o0) -tuples_on B2 = { w where w is Element of B2 * : len w = arity o0 } &
(arity o0) -tuples_on B1 = { v where v is Element of B1 * : len v = arity o0 } &
(arity o0) -tuples_on the
carrier of
U0 = { x where x is Element of the carrier of U0 * : len x = arity o0 } )
by FINSEQ_2:def 4;
A10:
(
B2 is_closed_on o0 &
B1 is_closed_on o0 )
by A2, Def5;
A11:
arity o2 = arity o0
by A8, Th9;
A12:
o2 =
o0 /. B2
by A2, A8, Def7
.=
o0 | ((arity o0) -tuples_on B2)
by A10, Def6
;
(
s0 in (arity o0) -tuples_on the
carrier of
U0 &
s2 in (arity o0) -tuples_on B2 &
s2 = s0 )
by A6, A9, A11;
then
o2 . s = o0 . s1
by A12, FUNCT_1:72;
hence
o2 . s in B
by A3, A6, A10, A11, Def4;
:: thesis: verum
end;
now let n be
Nat;
:: thesis: ( n in dom the charact of U0 implies the charact of U1 . n = (Opers U2,B) . n )assume A13:
n in dom the
charact of
U0
;
:: thesis: the charact of U1 . n = (Opers U2,B) . nthen reconsider o0 = the
charact of
U0 . n as
operation of
U0 by FUNCT_1:def 5;
reconsider o1 = the
charact of
U1 . n as
operation of
U1 by A4, A13, FUNCT_1:def 5;
reconsider o2 = the
charact of
U2 . n as
operation of
U2 by A4, A13, FUNCT_1:def 5;
A14:
(
o1 = o0 /. B1 &
o2 = o0 /. B2 )
by A2, A4, A13, Def7;
A15:
(
B1 is_closed_on o0 &
B2 is_closed_on o0 &
B is_closed_on o2 )
by A2, A5, Def5;
A16:
arity o2 = arity o0
by A4, A13, Th9;
thus the
charact of
U1 . n =
o0 /. B1
by A2, A4, A13, Def7
.=
o0 | ((arity o0) -tuples_on B1)
by A15, Def6
.=
o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1))
by A1, Th1
.=
(o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B)
by A3, RELAT_1:100
.=
(o0 /. B2) | ((arity o0) -tuples_on B)
by A15, Def6
.=
o2 /. B
by A14, A15, A16, Def6
.=
(Opers U2,B) . n
by A4, A13, Def7
;
:: thesis: verum end;
hence
the charact of U1 = Opers U2,B
by A4, FINSEQ_1:17; :: thesis: B is opers_closed
thus
B is opers_closed
by A5; :: thesis: verum