let x, y be PFuncFinSequence of {{}}; :: thesis: ( len x = len f & ( for n being Nat st n in dom x holds
for m being Nat st m = f . n holds
x . n = TrivialOp m ) & len y = len f & ( for n being Nat st n in dom y holds
for m being Nat st m = f . n holds
y . n = TrivialOp m ) implies x = y )
assume that
A3: len x = len f and
A4: for n being Nat st n in dom x holds
for m being Nat st m = f . n holds
x . n = TrivialOp m and
A5: len y = len f and
A6: for n being Nat st n in dom y holds
for m being Nat st m = f . n holds
y . n = TrivialOp m ; :: thesis: x = y
A7: dom x = Seg (len f) by A3, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom x holds
x . n = y . n

let n be Nat; :: thesis: ( n in dom x implies x . n = y . n )
assume A8: n in dom x ; :: thesis: x . n = y . n
then n in dom f by A7, FINSEQ_1:def 3;
then reconsider m = f . n as Element of NAT by FINSEQ_2:11;
( n in dom y & x . n = TrivialOp m ) by A4, A5, A7, A8, FINSEQ_1:def 3;
hence x . n = y . n by A6; :: thesis: verum

end;

hence x = y by A3, A5, FINSEQ_2:9; :: thesis: verum