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 object ; :: 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 and
A3: j in dom A and
A4: z in A . j by Def1;
A5: j in dom (Cut (A,i,x)) by A3, 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 A5, Def2;
hence z in union ((Cut (A,i,x)),J) by A2, A4, A5, Def1; :: thesis: verum

end;

end;

end;

let z be object ; :: 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
A6: j in J and
A7: j in dom (Cut (A,i,x)) and
A8: z in (Cut (A,i,x)) . j by Def1;
A9: j in dom A by A7, 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, A6; :: thesis: verum

end;

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

then (Cut (A,i,x)) . j = A . j by A7, Def2;
hence z in union (A,J) by A6, A8, A9, Def1; :: thesis: verum

end;

end;