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)) & 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)) & 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)) & 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)) & 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)) 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