defpred S₁[ set ] means (Partial_Intersection XSeq) . $1 in Si;
X: rng XSeq c= Si by PROB_1:def 9;
Y: XSeq . 0 in rng XSeq by NAT_1:52;
(Partial_Intersection XSeq) . 0 = XSeq . 0 by Def1;
then A1: S₁[ 0 ] by X, Y;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
Y: XSeq . (k + 1) in rng XSeq by NAT_1:52;
assume (Partial_Intersection XSeq) . k in Si ; :: thesis: S₁[k + 1]
then A3: (Partial_Intersection XSeq) . k is Event of Si ;
XSeq . (k + 1) in Si by X, Y;
then XSeq . (k + 1) is Event of Si ;
then ((Partial_Intersection XSeq) . k) /\ (XSeq . (k + 1)) is Event of Si by A3, PROB_1:49;
then ((Partial_Intersection XSeq) . k) /\ (XSeq . (k + 1)) in Si ;
hence S₁[k + 1] by Def1; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
then rng (Partial_Intersection XSeq) c= Si by NAT_1:53;
hence Partial_Intersection XSeq is SetSequence of Si by PROB_1:def 9; :: thesis: verum