let f1, f2 be PFuncFinSequence of (TS (DTConUA (f,D))); ( len f1 = len f & ( for n being Nat st n in dom f1 holds
f1 . n = FreeOpNSG (n,f,D) ) & len f2 = len f & ( for n being Nat st n in dom f2 holds
f2 . n = FreeOpNSG (n,f,D) ) implies f1 = f2 )
assume that
A3:
len f1 = len f
and
A4:
for n being Nat st n in dom f1 holds
f1 . n = FreeOpNSG (n,f,D)
and
A5:
len f2 = len f
and
A6:
for n being Nat st n in dom f2 holds
f2 . n = FreeOpNSG (n,f,D)
; f1 = f2
for n being Nat st n in dom f1 holds
f1 . n = f2 . n
hence
f1 = f2
by A3, A5, FINSEQ_2:9; verum