set A = TS (DTConUA f,D);
set AA = UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #);
A1:
len (FreeOpSeqNSG f,D) = len f
by Def12;
for n being Nat
for h being PartFunc of ((TS (DTConUA f,D)) * ),(TS (DTConUA f,D)) st n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) & h = the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n holds
h is quasi_total
proof
let n be
Nat;
:: thesis: for h being PartFunc of ((TS (DTConUA f,D)) * ),(TS (DTConUA f,D)) st n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) & h = the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n holds
h is quasi_total let h be
PartFunc of
((TS (DTConUA f,D)) * ),
(TS (DTConUA f,D));
:: thesis: ( n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) & h = the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n implies h is quasi_total )
assume
(
n in dom the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #) &
h = the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #)
. n )
;
:: thesis: h is quasi_total
then
h = FreeOpNSG n,
f,
D
by Def12;
hence
h is
quasi_total
;
:: thesis: verum
end;
then A3:
the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) is quasi_total
by UNIALG_1:def 5;
for n being Nat
for h being PartFunc of ((TS (DTConUA f,D)) * ),(TS (DTConUA f,D)) st n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) & h = the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n holds
h is homogeneous
proof
let n be
Nat;
:: thesis: for h being PartFunc of ((TS (DTConUA f,D)) * ),(TS (DTConUA f,D)) st n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) & h = the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n holds
h is homogeneous let h be
PartFunc of
((TS (DTConUA f,D)) * ),
(TS (DTConUA f,D));
:: thesis: ( n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) & h = the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n implies h is homogeneous )
assume
(
n in dom the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #) &
h = the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #)
. n )
;
:: thesis: h is homogeneous
then
h = FreeOpNSG n,
f,
D
by Def12;
hence
h is
homogeneous
;
:: thesis: verum
end;
then A4:
the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) is homogeneous
by UNIALG_1:def 4;
for n being set st n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) holds
not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n is empty
proof
let n be
set ;
:: thesis: ( n in dom the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) implies not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n is empty )
assume A5:
n in dom the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #)
;
:: thesis: not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) . n is empty
then reconsider n =
n as
Element of
NAT ;
the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #)
. n = FreeOpNSG n,
f,
D
by A5, Def12;
hence
not the
charact of
UAStr(#
(TS (DTConUA f,D)),
(FreeOpSeqNSG f,D) #)
. n is
empty
;
:: thesis: verum
end;
then A6:
not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) is with_zero
by FUNCT_1:def 15;
the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) <> {}
by A1;
hence
UAStr(# (TS (DTConUA f,D)),(FreeOpSeqNSG f,D) #) is strict Universal_Algebra
by A3, A4, A6, UNIALG_1:def 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum