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 set ; :: 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 consider j being set such that
A2: ( j in {i} & j in dom A & x in A . j ) by Def1;
thus x in A . i by A2, TARSKI:def 1; :: thesis: verum

end;

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

proof

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

end;