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; :: 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)),(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)); :: thesis: ( 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 ) ; :: thesis: h is quasi_total
then h = FreeOpZAO n,f,D by Def18;
hence h is quasi_total ; :: thesis: verum

end;

then A1: the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO 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)),(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; :: 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)),(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)); :: thesis: ( 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 ) ; :: thesis: h is homogeneous
then h = FreeOpZAO n,f,D by Def18;
hence h is homogeneous ; :: thesis: verum

end;

then A2: the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO 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)),(FreeOpSeqZAO f,D) #) holds
not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO f,D) #) . n is empty

proof

let n be set ; :: thesis: ( 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) #) ; :: thesis: not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO f,D) #) . n is empty
then reconsider n = n as Element of NAT ;
the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO f,D) #) . n = FreeOpZAO n,f,D by A3, Def18;
hence not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO f,D) #) . n is empty ; :: thesis: verum

end;

then A4: not the charact of UAStr(# (TS (DTConUA f,D)),(FreeOpSeqZAO f,D) #) is with_zero by FUNCT_1:def 15;
len (FreeOpSeqZAO f,D) = len f by Def18;
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 7, UNIALG_1:def 8, UNIALG_1:def 9; :: thesis: verum