set j = the Element of J;
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;
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));
( 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 that A1:
n in dom the
charact of
UAStr(#
(product (Carrier A)),
(ProdOpSeq A) #)
and A2:
the
charact of
UAStr(#
(product (Carrier A)),
(ProdOpSeq A) #)
. n = h
;
h is quasi_total
the
charact of
UAStr(#
(product (Carrier A)),
(ProdOpSeq A) #)
. n = [[:(ProdOp (A,n)):]]
by A1, Def22;
hence
h is
quasi_total
by A2;
verum
end;
then A3:
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is quasi_total
;
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;
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));
( 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 that A4:
n in dom the
charact of
UAStr(#
(product (Carrier A)),
(ProdOpSeq A) #)
and A5:
the
charact of
UAStr(#
(product (Carrier A)),
(ProdOpSeq A) #)
. n = h
;
h is homogeneous
the
charact of
UAStr(#
(product (Carrier A)),
(ProdOpSeq A) #)
. n = [[:(ProdOp (A,n)):]]
by A4, Def22;
hence
h is
homogeneous
by A5;
verum
end;
then A6:
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is homogeneous
;
for n being object 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
then A8:
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is non-empty
by FUNCT_1:def 9;
len the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) =
len (ComSign A)
by Def22
.=
len (signature (A . the Element of J))
by Def14
.=
len the charact of (A . the Element of J)
by UNIALG_1:def 4
;
then
the charact of UAStr(# (product (Carrier A)),(ProdOpSeq A) #) <> {}
;
hence
UAStr(# (product (Carrier A)),(ProdOpSeq A) #) is strict Universal_Algebra
by A3, A6, A8, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; verum