let F be finite set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: union (A,{i,j}) = (A . i) \/ (A . j)
thus union (A,{i,j}) c= (A . i) \/ (A . j) :: according to XBOOLE_0:def 10 :: thesis: (A . i) \/ (A . j) c= union (A,{i,j})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A,{i,j}) or x in (A . i) \/ (A . j) )
assume x in union (A,{i,j}) ; :: thesis: x in (A . i) \/ (A . j)
then consider k being set such that
A3: ( k in {i,j} & k in dom A & x in A . k ) by Def1;

per cases ( ( k = i & k in dom A & x in A . k ) or ( k = j & k in dom A & x in A . k ) ) by A3, TARSKI:def 2;

suppose ( k = i & k in dom A & x in A . k ) ; :: thesis: x in (A . i) \/ (A . j)

hence x in (A . i) \/ (A . j) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( k = j & k in dom A & x in A . k ) ; :: thesis: x in (A . i) \/ (A . j)

hence x in (A . i) \/ (A . j) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus (A . i) \/ (A . j) c= union (A,{i,j}) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A . i) \/ (A . j) or x in union (A,{i,j}) )
assume A4: x in (A . i) \/ (A . j) ; :: thesis: x in union (A,{i,j})

per cases ( x in A . i or x in A . j ) by A4, XBOOLE_0:def 3;

suppose A5: x in A . i ; :: thesis: x in union (A,{i,j})

i in {i,j} by TARSKI:def 2;
hence x in union (A,{i,j}) by A1, A5, Def1; :: thesis: verum

end;

suppose A6: x in A . j ; :: thesis: x in union (A,{i,j})

j in {i,j} by TARSKI:def 2;
hence x in union (A,{i,j}) by A2, A6, Def1; :: thesis: verum

end;

end;

end;