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

now :: thesis: for i being Nat st i in Seg n holds
ex F being SigmaField of (((Seg n) --> REAL) . i) st
( F = (L-Field n) . i & M . i is sigma_Measure of F )

let i be Nat; :: thesis: ( i in Seg n implies ex F being SigmaField of (((Seg n) --> REAL) . i) st
( F = (L-Field n) . i & M . i is sigma_Measure of F ) )
assume A2: i in Seg n ; :: thesis: ex F being SigmaField of (((Seg n) --> REAL) . i) st
( F = (L-Field n) . i & M . i is sigma_Measure of F )
then A3: ( (L-Field n) . i = L-Field & M . i = L-Meas & ((Seg n) --> REAL) . i = REAL ) by FUNCOP_1:7;
then reconsider F = L-Field as SigmaField of (((Seg n) --> REAL) . i) ;
take F = F; :: thesis: ( F = (L-Field n) . i & M . i is sigma_Measure of F )
thus F = (L-Field n) . i by A2, FUNCOP_1:7; :: thesis: M . i is sigma_Measure of F
thus M . i is sigma_Measure of F by A3; :: thesis: verum

end;

hence (Seg n) --> L-Meas is sigmaMeasureFamily of L-Field n by MEASUR13:def 8; :: thesis: verum