let f1, f2 be PFuncFinSequence of (TS (DTConUA (f,D))); :: thesis: ( 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) ; :: thesis: f1 = f2
for n being Nat st n in dom f1 holds
f1 . n = f2 . n

proof

let n be Nat; :: thesis: ( n in dom f1 implies f1 . n = f2 . n )
A7: ( dom f1 = Seg (len f1) & dom f2 = Seg (len f2) ) by FINSEQ_1:def 3;
assume A8: n in dom f1 ; :: thesis: f1 . n = f2 . n
then f1 . n = FreeOpNSG (n,f,D) by A4;
hence f1 . n = f2 . n by A3, A5, A6, A7, A8; :: thesis: verum

end;

hence f1 = f2 by A3, A5, FINSEQ_2:9; :: thesis: verum