consider j being Element of J;
set ua = UAStr(# (product (Carrier A)),(ProdOpSeq A) #);
set pr = product (Carrier A);
for n being Nat
for h being PartFunc of ((product (Carrier A)) * ),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is quasi_total

proof

let n be Nat; :: thesis: for h being PartFunc of ((product (Carrier A)) * ),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is quasi_total
let h be PartFunc of ((product (Carrier A)) * ),(product (Carrier A)); :: thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n implies h is quasi_total )
assume that
A1: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) and
A2: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ; :: thesis: h is quasi_total
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp A,n):]] by A1, Def23;
hence h is quasi_total by A2; :: thesis: verum

end;

then A3: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is quasi_total by MARGREL1:def 25;
for n being Nat
for h being PartFunc of ((product (Carrier A)) * ),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is homogeneous

proof

let n be Nat; :: thesis: for h being PartFunc of ((product (Carrier A)) * ),(product (Carrier A)) st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n holds
h is homogeneous
let h be PartFunc of ((product (Carrier A)) * ),(product (Carrier A)); :: thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & h = the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n implies h is homogeneous )
assume that
A4: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) and
A5: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ; :: thesis: h is homogeneous
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp A,n):]] by A4, Def23;
hence h is homogeneous by A5; :: thesis: verum

end;

then A6: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is homogeneous by MARGREL1:def 24;
for n being set st n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) holds
not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty

proof

let n be set ; :: thesis: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) implies not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty )
assume A7: n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) ; :: thesis: not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty
then reconsider n9 = n as Element of NAT ;
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp A,n9):]] by A7, Def23;
hence not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty ; :: thesis: verum

end;

then A8: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is non-empty by FUNCT_1:def 15;
len the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) = len (ComSign A) by Def23
.= len (signature (A . j)) by Def14
.= len the charact of (A . j) by UNIALG_1:def 11 ;
then the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) <> {} ;
hence UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra by A3, A6, A8, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum