let U0 be Universal_Algebra; 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; ( 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 Th10;
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def8;
assume A2:
the carrier of U1 c= the carrier of U2
; U1 is SubAlgebra of U2
hence
the carrier of U1 is Subset of U2
; UNIALG_2:def 8 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; ( B = the carrier of U1 implies ( the charact of U1 = Opers (U2,B) & B is opers_closed ) )
assume A3:
B = the carrier of U1
; ( the charact of U1 = Opers (U2,B) & B is opers_closed )
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def8;
A4:
the charact of U2 = Opers (U0,B2)
by Def8;
A5:
B2 is opers_closed
by Def8;
A6:
dom (Opers (U2,B)) = dom the charact of U2
by Def7;
A7:
dom the charact of U2 = dom the charact of U0
by Th10;
A8:
B1 is opers_closed
by Def8;
A9:
B is opers_closed
proof
let o2 be
operation of
U2;
UNIALG_2:def 5 B is_closed_on o2let s be
FinSequence of
B;
UNIALG_2:def 4 ( 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:11;
reconsider o0 = the
charact of
U0 . n as
operation of
U0 by A7, A10, FUNCT_1:def 5;
A12:
arity o2 = arity o0
by A10, A11, Th9;
rng s c= B
by FINSEQ_1:def 4;
then A13:
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;
rng s c= the
carrier of
U0
by A13, XBOOLE_1:1;
then
s is
FinSequence of the
carrier of
U0
by FINSEQ_1:def 4;
reconsider s1 =
s as
Element of
B1 * by A3, FINSEQ_1:def 11;
assume A14:
arity o2 = len s
;
o2 . s in B
set tb2 =
(arity o0) -tuples_on B2;
A15:
B2 is_closed_on o0
by A5, Def5;
A16:
o2 =
o0 /. B2
by A4, A10, A11, Def7
.=
o0 | ((arity o0) -tuples_on B2)
by A15, Def6
;
A17:
B1 is_closed_on o0
by A8, Def5;
(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 A14, A12;
then
o2 . s = o0 . s1
by A16, FUNCT_1:72;
hence
o2 . s in B
by A3, A14, A17, A12, Def4;
verum
end;
A18:
the charact of U1 = Opers (U0,B1)
by Def8;
now let n be
Nat;
( n in dom the charact of U0 implies the charact of U1 . n = (Opers (U2,B)) . n )assume A19:
n in dom the
charact of
U0
;
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 o2 = the
charact of
U2 . n as
operation of
U2 by A7, A19, FUNCT_1:def 5;
A20:
(
o2 = o0 /. B2 &
arity o2 = arity o0 )
by A4, A7, A19, Def7, Th9;
A21:
B is_closed_on o2
by A9, Def5;
A22:
B2 is_closed_on o0
by A5, Def5;
A23:
B1 is_closed_on o0
by A8, Def5;
thus the
charact of
U1 . n =
o0 /. B1
by A18, A1, A19, Def7
.=
o0 | ((arity o0) -tuples_on B1)
by A23, Def6
.=
o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1))
by A2, MARGREL1:57
.=
(o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B)
by A3, RELAT_1:100
.=
(o0 /. B2) | ((arity o0) -tuples_on B)
by A22, Def6
.=
o2 /. B
by A21, A20, Def6
.=
(Opers (U2,B)) . n
by A7, A6, A19, Def7
;
verum end;
hence
the charact of U1 = Opers (U2,B)
by A1, A7, A6, FINSEQ_1:17; B is opers_closed
thus
B is opers_closed
by A9; verum