let F be finite set ; :: thesis: for A being FinSequence of bool F
for i being Element of NAT st i in dom A holds
union (A,{i}) = A . i
let A be FinSequence of bool F; :: thesis: for i being Element of NAT st i in dom A holds
union (A,{i}) = A . i
let i be Element of NAT ; :: thesis: ( i in dom A implies union (A,{i}) = A . i )
assume A1: i in dom A ; :: thesis: union (A,{i}) = A . i
thus union (A,{i}) c= A . i :: according to XBOOLE_0:def 10 :: thesis: A . i c= union (A,{i})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A,{i}) or x in A . i )
assume x in union (A,{i}) ; :: thesis: x in A . i
then ex j being set st
( j in {i} & j in dom A & x in A . j ) by Def1;
hence x in A . i by TARSKI:def 1; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A . i or x in union (A,{i}) )
A2: i in {i} by TARSKI:def 1;
assume x in A . i ; :: thesis: x in union (A,{i})
hence x in union (A,{i}) by A1, A2, Def1; :: thesis: verum

end;