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 ;
A4: len (Opers (U1,U2)) = len the charact of U1 by ;
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; :: according to MARGREL1:def 24 :: 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 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 ;
reconsider h1 = the charact of U1 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by ;
h = [[:h1,h2:]] by A2, A7, A8, Def4;
hence h is quasi_total ; :: thesis: 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 ; :: 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 ;
reconsider h1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by ;
the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n = [[:h1,h2:]] by ;
hence not the charact of UAStr(# [: the carrier of U1, the carrier of U2:],(Opers (U1,U2)) #) . n is empty ; :: thesis: 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; :: according to MARGREL1:def 23 :: 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 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 ;
reconsider h1 = the charact of U1 . n as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by ;
h = [[:h1,h2:]] by A2, A12, A13, Def4;
hence h is homogeneous ; :: thesis: 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 ; :: thesis: verum