let U1 be Universal_Algebra; :: thesis: for E being Congruence of U1 holds UAStr(# (Class E),(QuotOpSeq U1,E) #) is strict Universal_Algebra
let E be Congruence of U1; :: thesis: 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;
:: 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 A1:
(
n in dom (QuotOpSeq U1,E) &
h = (QuotOpSeq U1,E) . n )
;
:: thesis: h is homogeneous
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
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 A1;
:: thesis: verum
end;
then A2:
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;
:: 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 A3:
(
n in dom (QuotOpSeq U1,E) &
h = (QuotOpSeq U1,E) . n )
;
:: thesis: h is quasi_total
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
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 A3, Def13;
hence
h is
quasi_total
by A3;
:: thesis: verum
end;
then A4:
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 ;
:: thesis: ( n in dom (QuotOpSeq U1,E) implies not (QuotOpSeq U1,E) . n is empty )
assume A5:
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 Def13;
then A6:
n in dom the
charact of
U1
by FINSEQ_1:def 3;
reconsider n =
n as
Element of
NAT by A5;
reconsider o = the
charact of
U1 . n as
operation of
U1 by A6, FUNCT_1:def 5;
(QuotOpSeq U1,E) . n = QuotOp o,
E
by A5, Def13;
hence
not
(QuotOpSeq U1,E) . n is
empty
;
:: thesis: verum
end;
then A7:
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 A2, A4, A7, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum