let x, y be object ; :: thesis: for A being set st x in A & not y in A holds
<*x,y*> - A = <*y*>
let A be set ; :: thesis: ( x in A & not y in A implies <*x,y*> - A = <*y*> )
assume that
A1: x in A and
A2: not y in A ; :: thesis: <*x,y*> - A = <*y*>
A3: <*y*> - A = <*y*> by A2, Lm6;
A4: <*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
<*x*> - A = {} by A1, Lm7;
hence <*x,y*> - A = {} ^ <*y*> by A3, A4, Lm11
.= <*y*> by FINSEQ_1:34 ;
:: thesis: verum