let n be non zero Nat; :: thesis: for D being n + 1 -element FinSequence
for D1 being n -element FinSequence st D1 = D | n holds
CarProduct D = [:(CarProduct D1),(D . (n + 1)):]
let D be n + 1 -element FinSequence; :: thesis: for D1 being n -element FinSequence st D1 = D | n holds
CarProduct D = [:(CarProduct D1),(D . (n + 1)):]
let D1 be n -element FinSequence; :: thesis: ( D1 = D | n implies CarProduct D = [:(CarProduct D1),(D . (n + 1)):] )
assume A1: D1 = D | n ; :: thesis: CarProduct D = [:(CarProduct D1),(D . (n + 1)):]
defpred S₁[ non zero Nat] means ( $1 <= n implies (ProdFinSeq D) . $1 = (ProdFinSeq D1) . $1 );
A2: S₁[1]

proof

assume 1 <= n ; :: thesis: (ProdFinSeq D) . 1 = (ProdFinSeq D1) . 1
then D . 1 = D1 . 1 by A1, FINSEQ_3:112;
then (ProdFinSeq D) . 1 = D1 . 1 by MEASUR13:def 3;
hence (ProdFinSeq D) . 1 = (ProdFinSeq D1) . 1 by MEASUR13:def 3; :: thesis: verum

end;

A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
assume A5: k + 1 <= n ; :: thesis: (ProdFinSeq D) . (k + 1) = (ProdFinSeq D1) . (k + 1)
then A6: k < n by NAT_1:13;
A7: D . (k + 1) = D1 . (k + 1) by A1, A5, FINSEQ_3:112;
k < n + 1 by A6, NAT_1:13;
then (ProdFinSeq D) . (k + 1) = [:((ProdFinSeq D) . k),(D . (k + 1)):] by MEASUR13:def 3;
hence (ProdFinSeq D) . (k + 1) = (ProdFinSeq D1) . (k + 1) by A6, A7, A4, MEASUR13:def 3; :: thesis: verum

end;

A8: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A2, A3);
n < n + 1 by NAT_1:13;
then CarProduct D = [:((ProdFinSeq D) . n),(D . (n + 1)):] by MEASUR13:def 3;
hence CarProduct D = [:(CarProduct D1),(D . (n + 1)):] by A8; :: thesis: verum