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 object ; :: 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 object ; :: 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;