let n be Nat; :: thesis:
let X be set ; :: thesis:
let A1 be SetSequence of X; :: thesis:
let x be object ; :: thesis:
defpred S₁[ Nat] means ( ( for k being Nat st k <= $1 holds
x in A1 . k ) implies x in (Partial_Intersection A1) . $1 );
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A2: ( ( for k being Nat st k <= i holds
x in A1 . k ) implies x in (Partial_Intersection A1) . i ) ; :: thesis:
assume for k being Nat st k <= i + 1 holds
x in A1 . k ; :: thesis:
then A3: ( ( for k being Nat st k <= i holds
x in A1 . k ) & x in A1 . (i + 1) ) by NAT_1:12;
(Partial_Intersection A1) . (i + 1) = ((Partial_Intersection A1) . i) /\ (A1 . (i + 1)) by Def1;
hence x in (Partial_Intersection A1) . (i + 1) by A2, A3, XBOOLE_0:def 4; :: thesis:

end;

thus ( x in (Partial_Intersection A1) . n implies for k being Nat st k <= n holds
x in A1 . k ) :: thesis:

proof

assume A4: x in (Partial_Intersection A1) . n ; :: thesis:
for k being Nat st k <= n holds
x in A1 . k

proof

A5: Partial_Intersection A1 is V74() by Th10;
let k be Nat; :: thesis:
assume A6: k <= n ; :: thesis:
A7: (Partial_Intersection A1) . k c= A1 . k by Th8;
(Partial_Intersection A1) . n c= (Partial_Intersection A1) . k by A6, A5, PROB_1:def 4;
then (Partial_Intersection A1) . n c= A1 . k by A7;
hence x in A1 . k by A4; :: thesis:

end;

hence for k being Nat st k <= n holds
x in A1 . k ; :: thesis:

end;

A8: S₁[ 0 ]

proof

assume for k being Nat st k <= 0 holds
x in A1 . k ; :: thesis:
then x in A1 . 0 ;
hence x in (Partial_Intersection A1) . 0 by Def1; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A1);
hence ( ( for k being Nat st k <= n holds
x in A1 . k ) implies x in (Partial_Intersection A1) . n ) ; :: thesis: