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