let p, q be FinSequence; :: thesis: for A being set
for k being Nat st len p = k + 1 & q = p | (Seg k) holds
( p . (k + 1) in A iff p - A = q - A )
let A be set ; :: thesis: for k being Nat st len p = k + 1 & q = p | (Seg k) holds
( p . (k + 1) in A iff p - A = q - A )
let k be Nat; :: thesis: ( len p = k + 1 & q = p | (Seg k) implies ( p . (k + 1) in A iff p - A = q - A ) )
assume that
A1: len p = k + 1 and
A2: q = p | (Seg k) ; :: thesis: ( p . (k + 1) in A iff p - A = q - A )
thus ( p . (k + 1) in A implies p - A = q - A ) :: thesis: ( p - A = q - A implies p . (k + 1) in A )

proof

assume A3: p . (k + 1) in A ; :: thesis: p - A = q - A
thus p - A = (q ^ <*(p . (k + 1))*>) - A by A1, A2, Th53
.= (q - A) ^ (<*(p . (k + 1))*> - A) by Lm11
.= (q - A) ^ {} by A3, Lm7
.= q - A by FINSEQ_1:34 ; :: thesis: verum

end;

assume that
A4: p - A = q - A and
A5: not p . (k + 1) in A ; :: thesis: contradiction
q - A = (q ^ <*(p . (k + 1))*>) - A by A1, A2, A4, Th53
.= (q - A) ^ (<*(p . (k + 1))*> - A) by Lm11
.= (q - A) ^ <*(p . (k + 1))*> by A5, Lm6 ;
hence contradiction by FINSEQ_1:87; :: thesis: verum