let U1, U2 be Universal_Algebra; ( U1,U2 are_similar implies UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra )
set C = UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #);
A1:
dom (Opers (U1,U2)) = Seg (len (Opers (U1,U2)))
by FINSEQ_1:def 3;
assume A2:
U1,U2 are_similar
; UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra
then A3:
( dom the charact of U2 = Seg (len the charact of U2) & len the charact of U2 = len the charact of U1 )
by FINSEQ_1:def 3, UNIALG_2:1;
A4:
len (Opers (U1,U2)) = len the charact of U1
by A2, Def4;
A5:
dom the charact of U1 = Seg (len the charact of U1)
by FINSEQ_1:def 3;
A6:
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is quasi_total
proof
let n be
Nat;
MARGREL1:def 24 for b1 being Element of bool [:( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #):] holds
( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b1 = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b1 is quasi_total )let h be
PartFunc of
( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the
carrier of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #);
( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or h is quasi_total )
assume that A7:
n in dom the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
and A8:
h = the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
. n
;
h is quasi_total
reconsider h2 = the
charact of
U2 . n as non
empty homogeneous quasi_total PartFunc of
( the carrier of U2 *), the
carrier of
U2 by A1, A4, A3, A7, MARGREL1:def 24;
reconsider h1 = the
charact of
U1 . n as non
empty homogeneous quasi_total PartFunc of
( the carrier of U1 *), the
carrier of
U1 by A1, A5, A4, A7, MARGREL1:def 24;
h = [[:h1,h2:]]
by A2, A7, A8, Def4;
hence
h is
quasi_total
;
verum
end;
A9:
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is non-empty
proof
let n be
object ;
FUNCT_1:def 9 ( not n in proj1 the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty )
set h = the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
. n;
assume A10:
n in dom the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
;
not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty
then reconsider m =
n as
Element of
NAT ;
reconsider h2 = the
charact of
U2 . m as non
empty homogeneous quasi_total PartFunc of
( the carrier of U2 *), the
carrier of
U2 by A1, A4, A3, A10, MARGREL1:def 24;
reconsider h1 = the
charact of
U1 . m as non
empty homogeneous quasi_total PartFunc of
( the carrier of U1 *), the
carrier of
U1 by A1, A5, A4, A10, MARGREL1:def 24;
the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
. n = [[:h1,h2:]]
by A2, A10, Def4;
hence
not the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
. n is
empty
;
verum
end;
A11:
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is homogeneous
proof
let n be
Nat;
MARGREL1:def 23 for b1 being Element of bool [:( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #):] holds
( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b1 = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b1 is homogeneous )let h be
PartFunc of
( the carrier of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) *), the
carrier of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #);
( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not h = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or h is homogeneous )
assume that A12:
n in dom the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
and A13:
h = the
charact of
UAStr(#
[: the carrier of U1, the carrier of U2:],
(Opers (U1,U2)) #)
. n
;
h is homogeneous
reconsider h2 = the
charact of
U2 . n as non
empty homogeneous quasi_total PartFunc of
( the carrier of U2 *), the
carrier of
U2 by A1, A4, A3, A12, MARGREL1:def 24;
reconsider h1 = the
charact of
U1 . n as non
empty homogeneous quasi_total PartFunc of
( the carrier of U1 *), the
carrier of
U1 by A1, A5, A4, A12, MARGREL1:def 24;
h = [[:h1,h2:]]
by A2, A12, A13, Def4;
hence
h is
homogeneous
;
verum
end;
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) <> {}
by A4;
hence
UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is strict Universal_Algebra
by A6, A11, A9, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; verum