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 = FreeOpZAO (n,f,D) ) & len f2 = len f & ( for n being Nat st n in dom f2 holds
f2 . n = FreeOpZAO (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 = FreeOpZAO (n,f,D) and
A5: len f2 = len f and
A6: for n being Nat st n in dom f2 holds
f2 . n = FreeOpZAO (n,f,D) ; :: thesis: f1 = f2
A7: dom f1 = Seg (len f1) by FINSEQ_1:def 3;
A8: dom f = Seg (len f) by FINSEQ_1:def 3;
A9: dom f2 = Seg (len f2) by FINSEQ_1:def 3;
for n being Nat st n in dom f holds
f1 . n = f2 . n
proof
let n be Nat; :: thesis: ( n in dom f implies f1 . n = f2 . n )
assume A10: n in dom f ; :: thesis: f1 . n = f2 . n
then f1 . n = FreeOpZAO (n,f,D) by A3, A4, A8, A7;
hence f1 . n = f2 . n by A5, A6, A8, A9, A10; :: thesis: verum
end;
hence f1 = f2 by A3, A5, A8, A7, FINSEQ_2:9; :: thesis: verum