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})
A1: dom (Cut A,i,x) = dom A by Def2;
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
A2: ( j in J \ {i} & j in dom (Cut A,i,x) & z in (Cut A,i,x) . j ) by Def1;
( j in J & not j in {i} & j in dom (Cut A,i,x) & z in (Cut A,i,x) . j ) by A2, XBOOLE_0:def 5;
then i <> j by TARSKI:def 1;
then ( j in J \ {i} & j in dom A & z in A . j ) by A2, Def2;
hence z in union A,(J \ {i}) by Def1; :: thesis: verum

end;

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
A3: ( j in J \ {i} & j in dom A & z in A . j ) by Def1;
( j in J & not j in {i} ) by A3, XBOOLE_0:def 5;
then i <> j by TARSKI:def 1;
then (Cut A,i,x) . j = A . j by A1, A3, Def2;
hence z in union (Cut A,i,x),(J \ {i}) by A1, A3, Def1; :: thesis: verum

end;