let U1 be Universal_Algebra; for E being Congruence of U1 holds UAStr(# (Class E),(QuotOpSeq U1,E) #) is strict Universal_Algebra
let E be Congruence of U1; UAStr(# (Class E),(QuotOpSeq U1,E) #) is strict Universal_Algebra
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 Def13;
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 5;
(QuotOpSeq U1,E) . n = QuotOp o,
E
by A1, Def13;
hence
h is
homogeneous
by A2;
verum
end;
then A3:
the charact of UAStr(# (Class E),(QuotOpSeq U1,E) #) is homogeneous
by UNIALG_1:def 4;
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 Def13;
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 5;
(QuotOpSeq U1,E) . n = QuotOp o,
E
by A4, Def13;
hence
h is
quasi_total
by A5;
verum
end;
then A6:
the charact of UAStr(# (Class E),(QuotOpSeq U1,E) #) is quasi_total
by UNIALG_1:def 5;
for n being set st n in dom (QuotOpSeq U1,E) holds
not (QuotOpSeq U1,E) . n is empty
proof
let n be
set ;
( 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 Def13;
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 5;
(QuotOpSeq U1,E) . n = QuotOp o,
E
by A7, Def13;
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 15;
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 7, UNIALG_1:def 8, UNIALG_1:def 9; verum