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

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;

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;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