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 Def17;
hence h is quasi_total ; :: thesis: 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; :: 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 Def17;
hence h is homogeneous ; :: thesis: 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 ; :: 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 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 ; :: thesis: 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; :: thesis: verum