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 A3: ( 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 ) ) ; :: thesis: x = y
X: dom x = Seg (len f) by A3, FINSEQ_1:def 3;

now

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

end;

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