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

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

hence
f = g
by A6, A8; :: thesis: verum
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;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