A2: ( len X = m & len S = m ) by CARD_1:def 7;
set Xn = SubFin (X,n);
set Sn = S | n;
A3: SubFin (X,n) = X | n by A1, Def5;
len (S | n) = n by FINSEQ_1:59, A2, A1;
then reconsider Sn = S | n as n -element FinSequence by CARD_1:def 7;
for i being Nat st i in Seg n holds
Sn . i is SigmaField of ((SubFin (X,n)) . i)

proof

let i be Nat; :: thesis: ( i in Seg n implies Sn . i is SigmaField of ((SubFin (X,n)) . i) )
assume A4: i in Seg n ; :: thesis: Sn . i is SigmaField of ((SubFin (X,n)) . i)
then A5: ( 1 <= i & i <= n ) by FINSEQ_1:1;
then i <= m by A1, XXREAL_0:2;
then A6: i in Seg m by A5;
( S . i = Sn . i & X . i = (SubFin (X,n)) . i ) by A4, A3, FUNCT_1:49;
hence Sn . i is SigmaField of ((SubFin (X,n)) . i) by A6, Def2; :: thesis: verum

end;

then reconsider Sn = Sn as sigmaFieldFamily of SubFin (X,n) by Def2;
Sn = S | n ;
hence S | n is sigmaFieldFamily of SubFin (X,n) ; :: thesis: verum