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