let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT
for x, J being set st not i in J holds
union A,J = union (Cut A,i,x),J
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for x, J being set st not i in J holds
union A,J = union (Cut A,i,x),J
let i be Element of NAT ; :: thesis: for x, J being set st not i in J holds
union A,J = union (Cut A,i,x),J
let x, J be set ; :: thesis: ( not i in J implies union A,J = union (Cut A,i,x),J )
assume A1: not i in J ; :: thesis: union A,J = union (Cut A,i,x),J
thus union A,J c= union (Cut A,i,x),J :: according to XBOOLE_0:def 10 :: thesis: union (Cut A,i,x),J c= union A,J

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union A,J or z in union (Cut A,i,x),J )
assume z in union A,J ; :: thesis: z in union (Cut A,i,x),J
then consider j being set such that
A2: ( j in J & j in dom A & z in A . j ) by Def1;
A3: j in dom (Cut A,i,x) by A2, Def2;

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

suppose i = j ; :: thesis: z in union (Cut A,i,x),J

hence z in union (Cut A,i,x),J by A1, A2; :: thesis: verum

end;

suppose i <> j ; :: thesis: z in union (Cut A,i,x),J

then (Cut A,i,x) . j = A . j by A3, Def2;
hence z in union (Cut A,i,x),J by A2, A3, Def1; :: thesis: verum

end;

end;

end;

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in union (Cut A,i,x),J or z in union A,J )
assume z in union (Cut A,i,x),J ; :: thesis: z in union A,J
then consider j being set such that
A4: ( j in J & j in dom (Cut A,i,x) & z in (Cut A,i,x) . j ) by Def1;
A5: j in dom A by A4, Def2;

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

suppose i = j ; :: thesis: z in union A,J

hence z in union A,J by A1, A4; :: thesis: verum

end;

suppose i <> j ; :: thesis: z in union A,J

then (Cut A,i,x) . j = A . j by A4, Def2;
hence z in union A,J by A4, A5, Def1; :: thesis: verum

end;

end;