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 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
; U1 is SubAlgebra of U2
hence
the carrier of U1 is Subset of U2
; UNIALG_2:def 7 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 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;
UNIALG_2:def 4 B is_closed_on o2let s be
FinSequence of
B;
UNIALG_2:def 3 ( 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 A7, A10, FUNCT_1:def 3;
A12:
arity o2 = arity o0
by A10, A11, Th6;
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 A3, FINSEQ_1:def 11;
assume A13:
arity o2 = len s
;
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 A14, Def5
;
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 A13, A12;
then
o2 . s = o0 . s1
by A15, FUNCT_1:49;
hence
o2 . s in B
by A3, A13, A16, A12;
verum
end;
A17:
the charact of U1 = Opers (U0,B1)
by Def7;
now for n being Nat st n in dom the charact of U0 holds
the charact of U1 . n = (Opers (U2,B)) . nlet n be
Nat;
( 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
;
the charact of U1 . n = (Opers (U2,B)) . nthen 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 A7, A18, FUNCT_1:def 3;
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 A22, Def5
.=
o0 | (((arity o0) -tuples_on B2) /\ ((arity o0) -tuples_on B1))
by A2, MARGREL1:21
.=
(o0 | ((arity o0) -tuples_on B2)) | ((arity o0) -tuples_on B)
by A3, RELAT_1:71
.=
(o0 /. B2) | ((arity o0) -tuples_on B)
by A21, Def5
.=
o2 /. B
by A20, A19, Def5
.=
(Opers (U2,B)) . n
by A7, A6, A18, Def6
;
verum end;
hence
the charact of U1 = Opers (U2,B)
by A1, A7, A6, FINSEQ_1:13; B is opers_closed
thus
B is opers_closed
by A9; verum