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