let n be non zero Nat; :: thesis: for D being n -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Interval ) holds
CarProduct D is Element of Prod_Field (L-Field n)
let D be n -element FinSequence; :: thesis: ( ( for i being Nat st i in Seg n holds
D . i is Interval ) implies CarProduct D is Element of Prod_Field (L-Field n) )
assume A1: for i being Nat st i in Seg n holds
D . i is Interval ; :: thesis: CarProduct D is Element of Prod_Field (L-Field n)

now :: thesis: for i being Nat st i in Seg n holds
D . i is Element of L-Field

let i be Nat; :: thesis: ( i in Seg n implies D . i is Element of L-Field )
assume i in Seg n ; :: thesis: D . i is Element of L-Field
then D . i is Interval by A1;
hence D . i is Element of L-Field by MEASUR12:72, MEASUR12:75; :: thesis: verum

end;

hence CarProduct D is Element of Prod_Field (L-Field n) by Th8; :: thesis: verum