let U0 be Universal_Algebra; :: thesis: for A being non empty Subset of U0 holds UAStr(# A,(Opers U0,A) #) is strict Universal_Algebra
let A be non empty Subset of U0; :: thesis: UAStr(# A,(Opers U0,A) #) is strict Universal_Algebra
set C = UAStr(# A,(Opers U0,A) #);
A1: dom the charact of UAStr(# A,(Opers U0,A) #) = dom the charact of U0 by Def7;
for n being Nat
for h being PartFunc of (the carrier of UAStr(# A,(Opers U0,A) #) * ),the carrier of UAStr(# A,(Opers U0,A) #) st n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n holds
h is homogeneous

proof

let n be Nat; :: thesis: for h being PartFunc of (the carrier of UAStr(# A,(Opers U0,A) #) * ),the carrier of UAStr(# A,(Opers U0,A) #) st n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n holds
h is homogeneous
let h be PartFunc of (the carrier of UAStr(# A,(Opers U0,A) #) * ),the carrier of UAStr(# A,(Opers U0,A) #); :: thesis: ( n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n implies h is homogeneous )
assume A2: ( n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n ) ; :: thesis: h is homogeneous
then reconsider o = the charact of U0 . n as operation of U0 by A1, FUNCT_1:def 5;
h = o /. A by A2, Def7;
hence h is homogeneous ; :: thesis: verum

end;

then A3: the charact of UAStr(# A,(Opers U0,A) #) is homogeneous by UNIALG_1:def 4;
for n being Nat
for h being PartFunc of UAStr(# A,(Opers U0,A) #) st n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n holds
h is quasi_total

proof

let n be Nat; :: thesis: for h being PartFunc of UAStr(# A,(Opers U0,A) #) st n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n holds
h is quasi_total
let h be PartFunc of (the carrier of UAStr(# A,(Opers U0,A) #) * ),the carrier of UAStr(# A,(Opers U0,A) #); :: thesis: ( n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n implies h is quasi_total )
assume A4: ( n in dom the charact of UAStr(# A,(Opers U0,A) #) & h = the charact of UAStr(# A,(Opers U0,A) #) . n ) ; :: thesis: h is quasi_total
then reconsider o = the charact of U0 . n as operation of U0 by A1, FUNCT_1:def 5;
h = o /. A by A4, Def7;
hence h is quasi_total ; :: thesis: verum

end;

then A5: the charact of UAStr(# A,(Opers U0,A) #) is quasi_total by UNIALG_1:def 5;
dom the charact of UAStr(# A,(Opers U0,A) #) <> {} by A1, RELAT_1:64;
then A6: the charact of UAStr(# A,(Opers U0,A) #) <> {} by RELAT_1:60;
for n being set st n in dom the charact of UAStr(# A,(Opers U0,A) #) holds
not the charact of UAStr(# A,(Opers U0,A) #) . n is empty

proof

let n be set ; :: thesis: ( n in dom the charact of UAStr(# A,(Opers U0,A) #) implies not the charact of UAStr(# A,(Opers U0,A) #) . n is empty )
assume A7: n in dom the charact of UAStr(# A,(Opers U0,A) #) ; :: thesis: not the charact of UAStr(# A,(Opers U0,A) #) . n is empty
then reconsider o = the charact of U0 . n as operation of U0 by A1, FUNCT_1:def 5;
the charact of UAStr(# A,(Opers U0,A) #) . n = o /. A by A7, Def7;
hence not the charact of UAStr(# A,(Opers U0,A) #) . n is empty ; :: thesis: verum

end;

then the charact of UAStr(# A,(Opers U0,A) #) is non-empty by FUNCT_1:def 15;
hence UAStr(# A,(Opers U0,A) #) is strict Universal_Algebra by A3, A5, A6, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum