set UU = UAStr(# (Class E),(QuotOpSeq (U1,E)) #);
for n being Nat
for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is homogeneous

proof

let n be Nat; :: thesis: for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is homogeneous
let h be PartFunc of ((Class E) *),(Class E); :: thesis: ( n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n implies h is homogeneous )
assume that
A1: n in dom (QuotOpSeq (U1,E)) and
A2: h = (QuotOpSeq (U1,E)) . n ; :: thesis: h is homogeneous
n in Seg (len (QuotOpSeq (U1,E))) by A1, FINSEQ_1:def 3;
then n in Seg (len the charact of U1) by Def9;
then n in dom the charact of U1 by FINSEQ_1:def 3;
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def 3;
(QuotOpSeq (U1,E)) . n = QuotOp (o,E) by A1, Def9;
hence h is homogeneous by A2; :: thesis: verum

end;

then A3: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is homogeneous ;
for n being Nat
for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is quasi_total

proof

let n be Nat; :: thesis: for h being PartFunc of ((Class E) *),(Class E) st n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n holds
h is quasi_total
let h be PartFunc of ((Class E) *),(Class E); :: thesis: ( n in dom (QuotOpSeq (U1,E)) & h = (QuotOpSeq (U1,E)) . n implies h is quasi_total )
assume that
A4: n in dom (QuotOpSeq (U1,E)) and
A5: h = (QuotOpSeq (U1,E)) . n ; :: thesis: h is quasi_total
n in Seg (len (QuotOpSeq (U1,E))) by A4, FINSEQ_1:def 3;
then n in Seg (len the charact of U1) by Def9;
then n in dom the charact of U1 by FINSEQ_1:def 3;
then reconsider o = the charact of U1 . n as operation of U1 by FUNCT_1:def 3;
(QuotOpSeq (U1,E)) . n = QuotOp (o,E) by A4, Def9;
hence h is quasi_total by A5; :: thesis: verum

end;

then A6: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is quasi_total ;
for n being object st n in dom (QuotOpSeq (U1,E)) holds
not (QuotOpSeq (U1,E)) . n is empty

proof

let n be object ; :: thesis: ( n in dom (QuotOpSeq (U1,E)) implies not (QuotOpSeq (U1,E)) . n is empty )
assume A7: n in dom (QuotOpSeq (U1,E)) ; :: thesis: not (QuotOpSeq (U1,E)) . n is empty
then n in Seg (len (QuotOpSeq (U1,E))) by FINSEQ_1:def 3;
then n in Seg (len the charact of U1) by Def9;
then A8: n in dom the charact of U1 by FINSEQ_1:def 3;
reconsider n = n as Element of NAT by A7;
reconsider o = the charact of U1 . n as operation of U1 by A8, FUNCT_1:def 3;
(QuotOpSeq (U1,E)) . n = QuotOp (o,E) by A7, Def9;
hence not (QuotOpSeq (U1,E)) . n is empty ; :: thesis: verum

end;

then A9: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is non-empty by FUNCT_1:def 9;
the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) <> {}

proof

assume A10: the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) = {} ; :: thesis: contradiction
len the charact of UAStr(# (Class E),(QuotOpSeq (U1,E)) #) = len the charact of U1 by Def9;
hence contradiction by A10; :: thesis: verum

end;

hence UAStr(# (Class E),(QuotOpSeq (U1,E)) #) is strict Universal_Algebra by A3, A6, A9, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; :: thesis: verum