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

proof

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

end;

assume A4: p - A = (q - A) ^ <*(p . (k + 1))*> ; :: thesis: not p . (k + 1) in A
assume p . (k + 1) in A ; :: thesis: contradiction
then q - A = (q - A) ^ <*(p . (k + 1))*> by A1, A2, A4, Th81;
hence contradiction by FINSEQ_1:87; :: thesis: verum