set A = TS (DTConUA (f,D));
set AA = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);
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))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds
h is quasi_total
proof
let n be
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))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds
h is quasi_total let h be
PartFunc of
((TS (DTConUA (f,D))) *),
(TS (DTConUA (f,D)));
( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n implies h is quasi_total )
assume
(
n in dom the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #) &
h = the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #)
. n )
;
h is quasi_total
then
h = FreeOpZAO (
n,
f,
D)
by Def17;
hence
h is
quasi_total
;
verum
end;
then A1:
the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is quasi_total
;
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))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds
h is homogeneous
proof
let n be
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))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n holds
h is homogeneous let h be
PartFunc of
((TS (DTConUA (f,D))) *),
(TS (DTConUA (f,D)));
( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) & h = the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n implies h is homogeneous )
assume
(
n in dom the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #) &
h = the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #)
. n )
;
h is homogeneous
then
h = FreeOpZAO (
n,
f,
D)
by Def17;
hence
h is
homogeneous
;
verum
end;
then A2:
the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is homogeneous
;
for n being object st n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) holds
not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty
proof
let n be
object ;
( n in dom the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) implies not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty )
assume A3:
n in dom the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #)
;
not the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) . n is empty
then reconsider n =
n as
Nat ;
the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #)
. n = FreeOpZAO (
n,
f,
D)
by A3, Def17;
hence
not the
charact of
UAStr(#
(TS (DTConUA (f,D))),
(FreeOpSeqZAO (f,D)) #)
. n is
empty
;
verum
end;
then A4:
the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is non-empty
by FUNCT_1:def 9;
len (FreeOpSeqZAO (f,D)) = len f
by Def17;
then
the charact of UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) <> {}
;
hence
UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is strict Universal_Algebra
by A1, A2, A4, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3; verum