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:3;
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;
UNIALG_1:def 5 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, UNIALG_1:5, UNIALG_1:def 5;
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, UNIALG_1:5, UNIALG_1:def 5;
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
set ;
FUNCT_1:def 15 ( 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, UNIALG_1:5, UNIALG_1:def 5;
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, UNIALG_1:5, UNIALG_1:def 5;
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;
UNIALG_1:def 4 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, UNIALG_1:5, UNIALG_1:def 5;
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, UNIALG_1:5, UNIALG_1:def 5;
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 7, UNIALG_1:def 8, UNIALG_1:def 9; verum