let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n
let X be set ; :: thesis: for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n
let A1 be SetSequence of X; :: thesis: (Partial_Intersection A1) . n c= A1 . n

per cases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: (Partial_Intersection A1) . n c= A1 . n

hence (Partial_Intersection A1) . n c= A1 . n by Def1; :: thesis: verum

end;

suppose ex k being Nat st n = k + 1 ; :: thesis: (Partial_Intersection A1) . n c= A1 . n

then consider k being Nat such that
A1: n = k + 1 ;
(Partial_Intersection A1) . (k + 1) = ((Partial_Intersection A1) . k) /\ (A1 . (k + 1)) by Def1;
hence (Partial_Intersection A1) . n c= A1 . n by A1, XBOOLE_1:17; :: thesis: verum

end;

end;