let f, g be FinSequence of Z_2; :: thesis: ( len f = len s & ( for j being Nat st 1 <= j & j <= len s holds
f . j = (s . j) @ x ) & len g = len s & ( for j being Nat st 1 <= j & j <= len s holds
g . j = (s . j) @ x ) implies f = g )
assume that
A6: len f = len s and
A7: for j being Nat st 1 <= j & j <= len s holds
f . j = (s . j) @ x and
A8: len g = len s and
A9: for j being Nat st 1 <= j & j <= len s holds
g . j = (s . j) @ x ; :: thesis: f = g
for k being Nat st 1 <= k & k <= len f holds
f . k = g . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len f implies f . k = g . k )
assume A10: ( 1 <= k & k <= len f ) ; :: thesis: f . k = g . k
f . k = (s . k) @ x by A6, A7, A10;
hence f . k = g . k by A6, A9, A10; :: thesis: verum

end;

hence f = g by A6, A8; :: thesis: verum