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 A1: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ) ; :: thesis: h is quasi_total
then the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp A,n):]] by Def23;
hence h is quasi_total by A1; :: thesis: verum

end;

then A2: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is quasi_total by UNIALG_1:def 5;
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 A3: ( n in dom the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) & the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = h ) ; :: thesis: h is homogeneous
then the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp A,n):]] by Def23;
hence h is homogeneous by A3; :: thesis: verum

end;

then A4: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is homogeneous by UNIALG_1:def 4;
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 A5: 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 n' = n as Element of NAT ;
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n = [[:(ProdOp A,n'):]] by A5, Def23;
hence not the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) . n is empty ; :: thesis: verum

end;

then A6: the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is non-empty by FUNCT_1:def 15;
consider j being Element of J;
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 A2, A4, A6, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum