let J be set ; :: thesis: for F being finite set
for i being Element of NAT
for A being FinSequence of bool F st i in J & i in dom A holds
union A,J = (union A,(J \ {i})) \/ (A . i)
let F be finite set ; :: thesis: for i being Element of NAT
for A being FinSequence of bool F st i in J & i in dom A holds
union A,J = (union A,(J \ {i})) \/ (A . i)
let i be Element of NAT ; :: thesis: for A being FinSequence of bool F st i in J & i in dom A holds
union A,J = (union A,(J \ {i})) \/ (A . i)
let A be FinSequence of bool F; :: thesis: ( i in J & i in dom A implies union A,J = (union A,(J \ {i})) \/ (A . i) )
assume ( i in J & i in dom A ) ; :: thesis: union A,J = (union A,(J \ {i})) \/ (A . i)
then A1: A . i c= union A,J by Th7;
thus union A,J c= (union A,(J \ {i})) \/ (A . i) :: according to XBOOLE_0:def 10 :: thesis: (union A,(J \ {i})) \/ (A . i) c= union A,J

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union A,J or x in (union A,(J \ {i})) \/ (A . i) )
assume x in union A,J ; :: thesis: x in (union A,(J \ {i})) \/ (A . i)
then consider j being set such that
A2: j in J and
A3: j in dom A and
A4: x in A . j by Def1;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: x in (union A,(J \ {i})) \/ (A . i)

hence x in (union A,(J \ {i})) \/ (A . i) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose i <> j ; :: thesis: x in (union A,(J \ {i})) \/ (A . i)

then not j in {i} by TARSKI:def 1;
then j in J \ {i} by A2, XBOOLE_0:def 5;
then x in union A,(J \ {i}) by A3, A4, Def1;
hence x in (union A,(J \ {i})) \/ (A . i) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus (union A,(J \ {i})) \/ (A . i) c= union A,J :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (union A,(J \ {i})) \/ (A . i) or x in union A,J )
assume x in (union A,(J \ {i})) \/ (A . i) ; :: thesis: x in union A,J
then A5: ( x in union A,(J \ {i}) or x in A . i ) by XBOOLE_0:def 3;

per cases ( x in union A,(J \ {i}) or x in union A,J ) by A1, A5;

suppose x in union A,(J \ {i}) ; :: thesis: x in union A,J

then ex j being set st
( j in J \ {i} & j in dom A & x in A . j ) by Def1;
hence x in union A,J by Def1; :: thesis: verum

end;

suppose x in union A,J ; :: thesis: x in union A,J

hence x in union A,J ; :: thesis: verum

end;

end;

end;