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 Element of L-Field ) 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 Element of L-Field ) 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 Element of L-Field ; :: thesis: CarProduct D is Element of Prod_Field (L-Field n)

per cases ( D is non-empty or not D is non-empty ) ;

suppose D is non-empty ; :: thesis: CarProduct D is Element of Prod_Field (L-Field n)

then reconsider D1 = D as non-empty n -element FinSequence ;
CarProduct D1 is Element of Prod_Field (L-Field n) by A1, MEASUR15:39;
hence CarProduct D is Element of Prod_Field (L-Field n) ; :: thesis: verum

end;

suppose not D is non-empty ; :: thesis: CarProduct D is Element of Prod_Field (L-Field n)

then CarProduct D = {} by Th6;
hence CarProduct D is Element of Prod_Field (L-Field n) by MEASURE1:7; :: thesis: verum

end;

end;