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 ) )
proof
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) )
proof
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;
thus ( ex k being Nat st
( k in dom F1 & x in F1 . k ) implies x in union (rng F1) ) :: thesis: verum
proof
given i being Nat such that A4: i in dom F1 and
A5: x in F1 . i ; :: thesis: x in union (rng F1)
F1 . i in rng F1 by A4, FUNCT_1:def 3;
hence x in union (rng F1) by A5, TARSKI:def 4; :: thesis: verum
end;
end;
union (rng F1) = Union F1 by CARD_3:def 4;
hence ( x in Union F1 iff ex k being Nat st
( k in dom F1 & x in F1 . k ) ) by A1; :: thesis: verum