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 A1: ( ( 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 = {} ) ) ; :: thesis: ( A1 . 0 = {} & Union A1 = Union F1 )
thus A1 . 0 = {} :: thesis: Union A1 = Union F1

proof

not 0 in dom F1 by Th1;
hence A1 . 0 = {} by A1; :: thesis: verum

end;

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 set ; :: 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 Element of NAT such that
A2: x in A1 . n by PROB_1:25;
A3: n in dom F1 by A1, A2;
x in F1 . n by A1, A2;
hence x in Union F1 by A3, Th54; :: thesis: verum

end;

let x be set ; :: 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 Th54;
A5: n in NAT by ORDINAL1:def 13;
x in A1 . n by A1, A4;
hence x in Union A1 by A5, PROB_1:25; :: thesis: verum

end;