let n be non zero Nat; :: thesis: for D being n -element FinSequence st not D is non-empty holds
CarProduct D = {}
let D be n -element FinSequence; :: thesis: ( not D is non-empty implies CarProduct D = {} )
assume not D is non-empty ; :: thesis: CarProduct D = {}
then consider i being object such that
A1: ( i in dom D & D . i = {} ) ;
reconsider i = i as Nat by A1;
A2: dom D = Seg n by FINSEQ_1:89;
then A3: ( 1 <= i & i <= n ) by A1, FINSEQ_1:1;
reconsider i = i as non zero Nat by A2, A1, FINSEQ_1:1;
defpred S₁[ non zero Nat] means ( i <= $1 & $1 <= n implies (ProdFinSeq D) . $1 = {} );
A4: S₁[1]

proof

assume ( i <= 1 & 1 <= n ) ; :: thesis: (ProdFinSeq D) . 1 = {}
then i = 1 by A3, XXREAL_0:1;
hence (ProdFinSeq D) . 1 = {} by A1, MEASUR13:def 3; :: thesis: verum

end;

A5: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
assume A7: ( i <= k + 1 & k + 1 <= n ) ; :: thesis: (ProdFinSeq D) . (k + 1) = {}
then A8: k < n by NAT_1:13;

per cases ( i = k + 1 or i <> k + 1 ) ;

suppose A9: i = k + 1 ; :: thesis: (ProdFinSeq D) . (k + 1) = {}

(ProdFinSeq D) . (k + 1) = [:((ProdFinSeq D) . k),(D . (k + 1)):] by A8, MEASUR13:def 3;
hence (ProdFinSeq D) . (k + 1) = {} by A1, A9; :: thesis: verum

end;

suppose i <> k + 1 ; :: thesis: (ProdFinSeq D) . (k + 1) = {}

then i < k + 1 by A7, XXREAL_0:1;
then (ProdFinSeq D) . (k + 1) = [:{},(D . (k + 1)):] by A6, A8, NAT_1:13, MEASUR13:def 3;
hence (ProdFinSeq D) . (k + 1) = {} ; :: thesis: verum

end;

end;

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A4, A5);
hence CarProduct D = {} by A3; :: thesis: verum