let x be object ; :: thesis: for X being set

for F1 being FinSequence of bool X holds

( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

let X be set ; :: thesis: for F1 being FinSequence of bool X holds

( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

let F1 be FinSequence of bool X; :: thesis: ( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

set Y = union (rng F1);

A1: for x being object holds

( x in union (rng F1) iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

hence ( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) ) by A1; :: thesis: verum

for F1 being FinSequence of bool X holds

( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

let X be set ; :: thesis: for F1 being FinSequence of bool X holds

( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

let F1 be FinSequence of bool X; :: thesis: ( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

set Y = union (rng F1);

A1: for x being object holds

( x in union (rng F1) iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

proof

union (rng F1) = Union F1
by CARD_3:def 4;
let x be object ; :: thesis: ( x in union (rng F1) iff ex k being Nat st

( k in dom F1 & x in F1 . k ) )

thus ( x in union (rng F1) implies ex k being Nat st

( k in dom F1 & x in F1 . k ) ) :: thesis: ( ex k being Nat st

( k in dom F1 & x in F1 . k ) implies x in union (rng F1) )

( k in dom F1 & x in F1 . k ) implies x in union (rng F1) ) :: thesis: verum

end;( k in dom F1 & x in F1 . k ) )

thus ( x in union (rng F1) implies ex k being Nat st

( k in dom F1 & x in F1 . k ) ) :: thesis: ( ex k being Nat st

( k in dom F1 & x in F1 . k ) implies x in union (rng F1) )

proof

thus
( ex k being Nat st
assume
x in union (rng F1)
; :: thesis: ex k being Nat st

( k in dom F1 & x in F1 . k )

then consider Z being set such that

A2: x in Z and

A3: Z in rng F1 by TARSKI:def 4;

ex i being Nat st

( i in dom F1 & Z = F1 . i ) by A3, FINSEQ_2:10;

hence ex k being Nat st

( k in dom F1 & x in F1 . k ) by A2; :: thesis: verum

end;( k in dom F1 & x in F1 . k )

then consider Z being set such that

A2: x in Z and

A3: Z in rng F1 by TARSKI:def 4;

ex i being Nat st

( i in dom F1 & Z = F1 . i ) by A3, FINSEQ_2:10;

hence ex k being Nat st

( k in dom F1 & x in F1 . k ) by A2; :: thesis: verum

( k in dom F1 & x in F1 . k ) implies x in union (rng F1) ) :: thesis: verum

hence ( x in Union F1 iff ex k being Nat st

( k in dom F1 & x in F1 . k ) ) by A1; :: thesis: verum