let X be set ; :: thesis: for F1 being FinSequence of bool X
for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) holds
( A1 . 0 = {} & Union A1 = Union F1 )
let F1 be FinSequence of bool X; :: thesis: for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) holds
( A1 . 0 = {} & Union A1 = Union F1 )
let A1 be SetSequence of X; :: thesis: ( ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) implies ( A1 . 0 = {} & Union A1 = Union F1 ) )
assume that
A1: for k being Nat st k in dom F1 holds
A1 . k = F1 . k and
A2: for k being Nat st not k in dom F1 holds
A1 . k = {} ; :: thesis: ( A1 . 0 = {} & Union A1 = Union F1 )
thus A1 . 0 = {} by A2, Th1; :: thesis: Union A1 = Union F1
thus Union A1 = Union F1 :: thesis: verum

proof

thus Union A1 c= Union F1 :: according to XBOOLE_0:def 10 :: thesis: Union F1 c= Union A1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union A1 or x in Union F1 )
assume x in Union A1 ; :: thesis: x in Union F1
then consider n being Nat such that
A3: x in A1 . n by PROB_1:12;
( n in dom F1 & x in F1 . n ) by A1, A2, A3;
hence x in Union F1 by Th49; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union F1 or x in Union A1 )
assume x in Union F1 ; :: thesis: x in Union A1
then consider n being Nat such that
A4: ( n in dom F1 & x in F1 . n ) by Th49;
( n in NAT & x in A1 . n ) by A1, A4;
hence x in Union A1 by PROB_1:12; :: thesis: verum

end;