let F be finite set ; 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; 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 ; 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 ; ( 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
; 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})
; verum