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;

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

hence
x = y
by A3, A5, FINSEQ_2:9; :: thesis: verumx . 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;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