let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds lim_inf (A1 (\) A) = (lim_inf A1) \ A
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds lim_inf (A1 (\) A) = (lim_inf A1) \ A
let A1 be SetSequence of X; :: thesis: lim_inf (A1 (\) A) = (lim_inf A1) \ A
reconsider X1 = inferior_setsequence A1 as SetSequence of X ;
reconsider X2 = inferior_setsequence (A1 (\) A) as SetSequence of X ;
X2 = X1 (\) A
proof
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: X2 . n = (X1 (\) A) . n
thus X2 . n = (X1 . n) \ A by Th53
.= (X1 (\) A) . n by Def8 ; :: thesis: verum
end;
then Union X2 = (Union X1) \ A by Th41;
then lim_inf (A1 (\) A) = (Union X1) \ A by SETLIM_1:def 4;
hence lim_inf (A1 (\) A) = (lim_inf A1) \ A by SETLIM_1:def 4; :: thesis: verum