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 i in dom (Cut A,i,x) & J c= dom (Cut A,i,x) & i in J holds
union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x})
let A be FinSequence of bool F; :: thesis: for i being Element of NAT
for x, J being set st i in dom (Cut A,i,x) & J c= dom (Cut A,i,x) & i in J holds
union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x})
let i be Element of NAT ; :: thesis: for x, J being set st i in dom (Cut A,i,x) & J c= dom (Cut A,i,x) & i in J holds
union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x})
let x, J be set ; :: thesis: ( i in dom (Cut A,i,x) & J c= dom (Cut A,i,x) & i in J implies union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x}) )
assume that
A1: ( i in dom (Cut A,i,x) & J c= dom (Cut A,i,x) ) and
A2: i in J ; :: thesis: union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x})
union (Cut A,i,x),J = (union (Cut A,i,x),(J \ {i})) \/ ((Cut A,i,x) . i) by A1, A2, Th8
.= (union A,(J \ {i})) \/ ((Cut A,i,x) . i) by Th12
.= (union A,(J \ {i})) \/ ((A . i) \ {x}) by A1, Def2 ;
hence union (Cut A,i,x),J = (union A,(J \ {i})) \/ ((A . i) \ {x}) ; :: thesis: verum