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 set ; :: 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 set ; :: 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;