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

proof

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

now :: thesis: for m being Nat st m in dom p1 holds
p1 . m = p2 . m

let m be Nat; :: thesis: ( m in dom p1 implies p1 . m = p2 . m )
assume A6: m in dom p1 ; :: thesis: p1 . m = p2 . m
then p1 . m = p . (m + n) by A3;
hence p1 . m = p2 . m by A2, A4, A5, A6; :: thesis: verum

end;

hence p1 = p2 by A2, A4; :: thesis: verum

end;