let X be set ; :: thesis:
let Si be SigmaField of X; :: thesis:
let FSi be FinSequence of Si; :: thesis:
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

proof

let n be Nat; :: thesis:

per cases ;

suppose not n in dom FSi ; :: thesis:

then A1 . n = {} by A2;
hence A1 . n in Si by PROB_1:4; :: thesis:

end;

suppose n in dom FSi ; :: thesis:

then A1 . n = FSi . n by A1;
hence A1 . n in Si ; :: thesis:

end;

end;

end;

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:
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: