let X be set ; :: thesis: for Si being SigmaField of X

for FSi being FinSequence of Si ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

let Si be SigmaField of X; :: thesis: for FSi being FinSequence of Si ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

let FSi be FinSequence of Si; :: thesis: ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

consider A1 being SetSequence of X such that

A1: for k being Nat st k in dom FSi holds

A1 . k = FSi . k and

A2: for k being Nat st not k in dom FSi holds

A1 . k = {} by Th54;

for n being Nat holds A1 . n in Si then rng A1 c= Si by NAT_1:52;

then reconsider A1 = A1 as SetSequence of Si by RELAT_1:def 19;

take A1 ; :: thesis: ( ( for k being Nat st k in dom FSi holds

A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

A1 . k = {} ) )

thus ( ( for k being Nat st k in dom FSi holds

A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

A1 . k = {} ) ) by A1, A2; :: thesis: verum

for FSi being FinSequence of Si ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

let Si be SigmaField of X; :: thesis: for FSi being FinSequence of Si ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

let FSi be FinSequence of Si; :: thesis: ex ASeq being SetSequence of Si st

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) )

consider A1 being SetSequence of X such that

A1: for k being Nat st k in dom FSi holds

A1 . k = FSi . k and

A2: for k being Nat st not k in dom FSi holds

A1 . k = {} by Th54;

for n being Nat holds A1 . n in Si then rng A1 c= Si by NAT_1:52;

then reconsider A1 = A1 as SetSequence of Si by RELAT_1:def 19;

take A1 ; :: thesis: ( ( for k being Nat st k in dom FSi holds

A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

A1 . k = {} ) )

thus ( ( for k being Nat st k in dom FSi holds

A1 . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

A1 . k = {} ) ) by A1, A2; :: thesis: verum