let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT
for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
let i be Element of NAT ; :: thesis: for x, J being set holds union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
let x, J be set ; :: thesis: union ((Cut (A,i,x)),(J \ {i})) = union (A,(J \ {i}))
thus union ((Cut (A,i,x)),(J \ {i})) c= union (A,(J \ {i})) :: according to XBOOLE_0:def 10 :: thesis: union (A,(J \ {i})) c= union ((Cut (A,i,x)),(J \ {i}))

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union ((Cut (A,i,x)),(J \ {i})) or z in union (A,(J \ {i})) )
assume z in union ((Cut (A,i,x)),(J \ {i})) ; :: thesis: z in union (A,(J \ {i}))
then consider j being set such that
A1: j in J \ {i} and
A2: j in dom (Cut (A,i,x)) and
A3: z in (Cut (A,i,x)) . j by Def1;
not j in {i} by A1, XBOOLE_0:def 5;
then i <> j by TARSKI:def 1;
then A4: z in A . j by A2, A3, Def2;
j in dom A by A2, Def2;
hence z in union (A,(J \ {i})) by A1, A4, Def1; :: thesis: verum

end;

A5: dom (Cut (A,i,x)) = dom A by Def2;
thus union (A,(J \ {i})) c= union ((Cut (A,i,x)),(J \ {i})) :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (A,(J \ {i})) or z in union ((Cut (A,i,x)),(J \ {i})) )
assume z in union (A,(J \ {i})) ; :: thesis: z in union ((Cut (A,i,x)),(J \ {i}))
then consider j being set such that
A6: j in J \ {i} and
A7: j in dom A and
A8: z in A . j by Def1;
not j in {i} by A6, XBOOLE_0:def 5;
then i <> j by TARSKI:def 1;
then (Cut (A,i,x)) . j = A . j by A5, A7, Def2;
hence z in union ((Cut (A,i,x)),(J \ {i})) by A5, A6, A7, A8, Def1; :: thesis: verum

end;