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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A,(({i} \/ J1) \/ J2)) or x in (A . i) \/ (union (A,(J1 \/ J2))) )
assume x in union (A,(({i} \/ J1) \/ J2)) ; :: thesis: x in (A . i) \/ (union (A,(J1 \/ J2)))
then consider j being set such that
A2: j in ({i} \/ J1) \/ J2 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 (A . i) \/ (union (A,(J1 \/ J2)))

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

end;

suppose A5: i <> j ; :: thesis: x in (A . i) \/ (union (A,(J1 \/ J2)))

j in {i} \/ (J1 \/ J2) by A2, XBOOLE_1:4;
then ( j in {i} or j in J1 \/ J2 ) by XBOOLE_0:def 3;
then x in union (A,(J1 \/ J2)) by A3, A4, A5, Def1, TARSKI:def 1;
hence x in (A . i) \/ (union (A,(J1 \/ J2))) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A . i) \/ (union (A,(J1 \/ J2))) or x in union (A,(({i} \/ J1) \/ J2)) )
assume A6: x in (A . i) \/ (union (A,(J1 \/ J2))) ; :: thesis: x in union (A,(({i} \/ J1) \/ J2))

per cases ( x in union (A,{i}) or x in union (A,(J1 \/ J2)) ) by A1, A6, XBOOLE_0:def 3;

suppose x in union (A,{i}) ; :: thesis: x in union (A,(({i} \/ J1) \/ J2))

then consider j being set such that
A7: j in {i} and
A8: ( j in dom A & x in A . j ) by Def1;
j in {i} \/ (J1 \/ J2) by A7, XBOOLE_0:def 3;
then j in ({i} \/ J1) \/ J2 by XBOOLE_1:4;
hence x in union (A,(({i} \/ J1) \/ J2)) by A8, Def1; :: thesis: verum

end;

suppose x in union (A,(J1 \/ J2)) ; :: thesis: x in union (A,(({i} \/ J1) \/ J2))

then consider j being set such that
A9: j in J1 \/ J2 and
A10: ( j in dom A & x in A . j ) by Def1;
j in {i} \/ (J1 \/ J2) by A9, XBOOLE_0:def 3;
then j in ({i} \/ J1) \/ J2 by XBOOLE_1:4;
hence x in union (A,(({i} \/ J1) \/ J2)) by A10, Def1; :: thesis: verum

end;

end;

end;