set j = the 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, Def22;
hence h is quasi_total by A2; :: thesis: verum

end;

then A3: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is quasi_total ;
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, Def22;
hence h is homogeneous by A5; :: thesis: verum

end;

then A6: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is homogeneous ;
for n being object 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 object ; :: 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, Def22;
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 9;
len the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) = len (ComSign A) by Def22
.= len (signature (A . the Element of J)) by Def14
.= len the charact of (A . the Element of J) by UNIALG_1:def 4 ;
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 1, UNIALG_1:def 2, UNIALG_1:def 3; :: thesis: verum