let U1, U2 be Universal_Algebra; :: thesis: ( U1,U2 are_similar implies UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) is strict Universal_Algebra )
assume A1:
U1,U2 are_similar
; :: thesis: 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) #);
A2:
( dom (Opers U1,U2) = Seg (len (Opers U1,U2)) & dom the charact of U1 = Seg (len the charact of U1) & dom the charact of U2 = Seg (len the charact of U2) )
by FINSEQ_1:def 3;
A3:
( len (Opers U1,U2) = len the charact of U1 & len the charact of U2 = len the charact of U1 )
by A1, Def4, UNIALG_2:3;
A4:
the charact of UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) is quasi_total
proof
let n be
Nat;
:: according to UNIALG_1:def 5 :: thesis: 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) #);
:: thesis: ( 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 A5:
(
n in dom the
charact of
UAStr(#
[:the carrier of U1,the carrier of U2:],
(Opers U1,U2) #) &
h = the
charact of
UAStr(#
[:the carrier of U1,the carrier of U2:],
(Opers U1,U2) #)
. n )
;
:: thesis: h is quasi_total
then reconsider h1 = the
charact of
U1 . n as non
empty homogeneous quasi_total PartFunc of
(the carrier of U1 * ),the
carrier of
U1 by A2, A3, UNIALG_1:5, UNIALG_1:def 5;
reconsider h2 = the
charact of
U2 . n as non
empty homogeneous quasi_total PartFunc of
(the carrier of U2 * ),the
carrier of
U2 by A2, A3, A5, UNIALG_1:5, UNIALG_1:def 5;
h = [[:h1,h2:]]
by A1, A5, Def4;
hence
h is
quasi_total
;
:: thesis: verum
end;
A6:
the charact of UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) is homogeneous
proof
let n be
Nat;
:: according to UNIALG_1:def 4 :: thesis: 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) #);
:: thesis: ( 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 A7:
(
n in dom the
charact of
UAStr(#
[:the carrier of U1,the carrier of U2:],
(Opers U1,U2) #) &
h = the
charact of
UAStr(#
[:the carrier of U1,the carrier of U2:],
(Opers U1,U2) #)
. n )
;
:: thesis: h is homogeneous
then reconsider h1 = the
charact of
U1 . n as non
empty homogeneous quasi_total PartFunc of
(the carrier of U1 * ),the
carrier of
U1 by A2, A3, UNIALG_1:5, UNIALG_1:def 5;
reconsider h2 = the
charact of
U2 . n as non
empty homogeneous quasi_total PartFunc of
(the carrier of U2 * ),the
carrier of
U2 by A2, A3, A7, UNIALG_1:5, UNIALG_1:def 5;
h = [[:h1,h2:]]
by A1, A7, Def4;
hence
h is
homogeneous
;
:: thesis: verum
end;
A8:
the charact of UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) <> {}
by A3;
the charact of UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) is non-empty
proof
let n be
set ;
:: according to FUNCT_1:def 15 :: thesis: ( 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 A9:
n in dom the
charact of
UAStr(#
[:the carrier of U1,the carrier of U2:],
(Opers U1,U2) #)
;
:: thesis: 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 h1 = the
charact of
U1 . m as non
empty homogeneous quasi_total PartFunc of
(the carrier of U1 * ),the
carrier of
U1 by A2, A3, A9, UNIALG_1:5, UNIALG_1:def 5;
reconsider h2 = the
charact of
U2 . m as non
empty homogeneous quasi_total PartFunc of
(the carrier of U2 * ),the
carrier of
U2 by A2, A3, A9, 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 A1, A9, Def4;
hence
not the
charact of
UAStr(#
[:the carrier of U1,the carrier of U2:],
(Opers U1,U2) #)
. n is
empty
;
:: thesis: verum
end;
hence
UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) is strict Universal_Algebra
by A4, A6, A8, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum