let n, k be non zero Nat; :: thesis: for X being non empty set
for D being n -element FinSequence st k in Seg n & ( for i being Nat st i in Seg n holds
D . i is Subset of X ) holds
(ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X))
let X be non empty set ; :: thesis: for D being n -element FinSequence st k in Seg n & ( for i being Nat st i in Seg n holds
D . i is Subset of X ) holds
(ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X))
let D be n -element FinSequence; :: thesis: ( k in Seg n & ( for i being Nat st i in Seg n holds
D . i is Subset of X ) implies (ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X)) )
assume that
A1: k in Seg n and
A2: for i being Nat st i in Seg n holds
D . i is Subset of X ; :: thesis: (ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X))
defpred S₁[ non zero Nat] means ( $1 in Seg n implies (ProdFinSeq D) . $1 is Subset of (CarProduct ((Seg $1) --> X)) );
A3: S₁[1]

proof

assume 1 in Seg n ; :: thesis: (ProdFinSeq D) . 1 is Subset of (CarProduct ((Seg 1) --> X))
then A4: D . 1 is Subset of X by A2;
1 in Seg 1 ;
then A5: ((Seg 1) --> X) . 1 = X by FUNCOP_1:7;
(ProdFinSeq D) . 1 = D . 1 by MEASUR13:def 3;
hence (ProdFinSeq D) . 1 is Subset of (CarProduct ((Seg 1) --> X)) by A4, A5, MEASUR13:def 3; :: thesis: verum

end;

A6: for i being non zero Nat st S₁[i] holds
S₁[i + 1]

proof

let i be non zero Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
assume A8: i + 1 in Seg n ; :: thesis: (ProdFinSeq D) . (i + 1) is Subset of (CarProduct ((Seg (i + 1)) --> X))
then ( 1 <= i + 1 & i + 1 <= n ) by FINSEQ_1:1;
then A9: ( 1 <= i & i < n ) by NAT_1:13, NAT_1:14;
((Seg (i + 1)) --> X) | i = ((Seg (i + 1)) /\ (Seg i)) --> X by FUNCOP_1:12;
then A10: (Seg i) --> X = ((Seg (i + 1)) --> X) | i by FINSEQ_3:18, XBOOLE_1:28;
( i < i + 1 & ((Seg (i + 1)) --> X) | (i + 1) = (Seg (i + 1)) --> X ) by NAT_1:16;
then A11: (ProdFinSeq D) . i is Subset of ((ProdFinSeq ((Seg (i + 1)) --> X)) . i) by A7, A9, A10, Th3;
((Seg (i + 1)) --> X) . (i + 1) = X by FINSEQ_1:4, FUNCOP_1:7;
then A12: D . (i + 1) is Subset of (((Seg (i + 1)) --> X) . (i + 1)) by A2, A8;
A13: (ProdFinSeq D) . (i + 1) = [:((ProdFinSeq D) . i),(D . (i + 1)):] by A9, MEASUR13:def 3;
CarProduct ((Seg (i + 1)) --> X) = [:((ProdFinSeq ((Seg (i + 1)) --> X)) . i),(((Seg (i + 1)) --> X) . (i + 1)):] by NAT_1:16, MEASUR13:def 3;
hence (ProdFinSeq D) . (i + 1) is Subset of (CarProduct ((Seg (i + 1)) --> X)) by A13, A11, A12, ZFMISC_1:96; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A3, A6);
hence (ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X)) by A1; :: thesis: verum