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 )

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 ; :: thesis: 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

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; :: thesis: verum

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 ; :: thesis: 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

A9:
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is non-empty
let n be Nat; :: according to MARGREL1:def 24 :: thesis: for b_{1} 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 b_{1} = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b_{1} 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 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 ; :: thesis: 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 ; :: thesis: verum

end;( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b

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 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 ; :: thesis: 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 ; :: thesis: verum

proof

A11:
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) is homogeneous
let n be object ; :: according to FUNCT_1:def 9 :: 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 A10: 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 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 ; :: thesis: verum

end;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)) #) ; :: 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 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 ; :: thesis: verum

proof

the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) <> {}
by A4;
let n be Nat; :: according to MARGREL1:def 23 :: thesis: for b_{1} 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 b_{1} = the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n or b_{1} 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 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 ; :: thesis: 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 ; :: thesis: verum

end;( not n in dom the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) or not b

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 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 ; :: thesis: 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 ; :: thesis: verum

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; :: thesis: verum