let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT
for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
let i be Element of NAT ; :: thesis: for x, y being set st x <> y & x in A . i & y in A . i holds
((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
let x, y be set ; :: thesis: ( x <> y & x in A . i & y in A . i implies ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i )
assume that
A1: x <> y and
A2: x in A . i and
A3: y in A . i ; :: thesis: ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i
A . i c= ((A . i) \ {x}) \/ ((A . i) \ {y})

proof

{} = {y} \ ({y} \/ {}) by XBOOLE_1:46;
then A . i = (A . i) \ ({y} \ {y}) ;
then A . i = ((A . i) \ {y}) \/ ((A . i) /\ {y}) by XBOOLE_1:52;
then A4: A . i = ((A . i) \ {y}) \/ {y} by A3, ZFMISC_1:46;
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in A . i or z in ((A . i) \ {x}) \/ ((A . i) \ {y}) )
not x in {y} by A1, TARSKI:def 1;
then A5: x in (A . i) \ {y} by A2, XBOOLE_0:def 5;
assume z in A . i ; :: thesis: z in ((A . i) \ {x}) \/ ((A . i) \ {y})
then z in (((A . i) \ {x}) \/ {x}) \/ (((A . i) \ {y}) \/ {y}) by A4, XBOOLE_0:def 3;
then z in ((A . i) \ {x}) \/ ({x} \/ ({y} \/ ((A . i) \ {y}))) by XBOOLE_1:4;
then z in ((A . i) \ {x}) \/ (({x} \/ {y}) \/ ((A . i) \ {y})) by XBOOLE_1:4;
then z in (((A . i) \ {x}) \/ ({y} \/ {x})) \/ ((A . i) \ {y}) by XBOOLE_1:4;
then z in ((((A . i) \ {x}) \/ {y}) \/ {x}) \/ ((A . i) \ {y}) by XBOOLE_1:4;
then A6: z in (((A . i) \ {x}) \/ {y}) \/ ({x} \/ ((A . i) \ {y})) by XBOOLE_1:4;
not y in {x} by A1, TARSKI:def 1;
then y in (A . i) \ {x} by A3, XBOOLE_0:def 5;
then z in ((A . i) \ {x}) \/ ({x} \/ ((A . i) \ {y})) by A6, ZFMISC_1:40;
hence z in ((A . i) \ {x}) \/ ((A . i) \ {y}) by A5, ZFMISC_1:40; :: thesis: verum

end;

hence ((A . i) \ {x}) \/ ((A . i) \ {y}) = A . i by XBOOLE_0:def 10; :: thesis: verum