let n be non zero Nat; :: thesis: (Seg n) --> L-Field is sigmaFieldFamily of (Seg n) --> REAL
set S = (Seg n) --> L-Field;
set X = (Seg n) --> REAL;
A1: dom ((Seg n) --> L-Field) = Seg n ;
reconsider S = (Seg n) --> L-Field as FinSequence ;
n is Element of NAT by ORDINAL1:def 12;
then len S = n by A1, FINSEQ_1:def 3;
then reconsider S = S as n -element FinSequence by CARD_1:def 7;

now :: thesis: for i being Nat st i in Seg n holds
S . i is SigmaField of (((Seg n) --> REAL) . i)

let i be Nat; :: thesis: ( i in Seg n implies S . i is SigmaField of (((Seg n) --> REAL) . i) )
assume i in Seg n ; :: thesis: S . i is SigmaField of (((Seg n) --> REAL) . i)
then ( S . i = L-Field & ((Seg n) --> REAL) . i = REAL ) by FUNCOP_1:7;
hence S . i is SigmaField of (((Seg n) --> REAL) . i) ; :: thesis: verum

end;

hence (Seg n) --> L-Field is sigmaFieldFamily of (Seg n) --> REAL by MEASUR13:def 2; :: thesis: verum