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

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

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;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union F1 or x in Union A1 )
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;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

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