let p, q be FinSequence; :: thesis: for A being set
for k being natural number 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 natural number 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 natural number ; :: 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 A1: ( len p = k + 1 & 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 A2: not p . (k + 1) in A ; :: thesis: p - A = (q - A) ^ <*(p . (k + 1))*>
thus p - A = (q ^ <*(p . (k + 1))*>) - A by A1, Th61
.= (q - A) ^ (<*(p . (k + 1))*> - A) by Lm11
.= (q - A) ^ <*(p . (k + 1))*> by A2, Lm6 ; :: thesis: verum

end;

assume A3: 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, A3, Th90;
hence contradiction by TREES_1:5; :: thesis: verum