let J be set ; for F being finite set
for i being Element of NAT
for A being FinSequence of bool F st i in J & i in dom A holds
union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
let F be finite set ; for i being Element of NAT
for A being FinSequence of bool F st i in J & i in dom A holds
union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
let i be Element of NAT ; for A being FinSequence of bool F st i in J & i in dom A holds
union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
let A be FinSequence of bool F; ( i in J & i in dom A implies union (A,J) = (union (A,(J \ {i}))) \/ (A . i) )
assume
( i in J & i in dom A )
; union (A,J) = (union (A,(J \ {i}))) \/ (A . i)
then A1:
A . i c= union (A,J)
by Th7;
thus
union (A,J) c= (union (A,(J \ {i}))) \/ (A . i)
XBOOLE_0:def 10 (union (A,(J \ {i}))) \/ (A . i) c= union (A,J)
thus
(union (A,(J \ {i}))) \/ (A . i) c= union (A,J)
verum