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;
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);
( 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
;
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;
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;
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);
( 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
;
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;
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 ;
( n in dom (QuotOpSeq (U1,E)) implies not (QuotOpSeq (U1,E)) . n is empty )
assume A7:
n in dom (QuotOpSeq (U1,E))
;
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
;
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)) #) <> {}
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; verum