let p1, p2 be XFinSequence; :: thesis: ( len p1 = (len f) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) & len p2 = (len f) -' n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) implies p1 = p2 )
thus ( len p1 = (len f) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) & len p2 = (len f) -' n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) implies p1 = p2 ) :: thesis: verum

proof

assume that
A2: ( len p1 = (len f) -' n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) ) and
A3: ( len p2 = (len f) -' n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) ) ; :: thesis: p1 = p2

now

let m be Nat; :: thesis: ( m in len p1 implies p1 . m = p2 . m )
assume m in len p1 ; :: thesis: p1 . m = p2 . m
then ( p1 . m = f . (m + n) & p2 . m = f . (m + n) ) by A2, A3;
hence p1 . m = p2 . m ; :: thesis: verum

end;

hence p1 = p2 by A2, A3, Th10; :: thesis: verum

end;