the point-map of F .: K c= the Points of S2

proof

hence
the point-map of F .: K is Subset of the Points of S2
; :: thesis: verum
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in the point-map of F .: K or b in the Points of S2 )

assume b in the point-map of F .: K ; :: thesis: b in the Points of S2

then ex a being object st

( a in dom the point-map of F & a in K & b = the point-map of F . a ) by FUNCT_1:def 6;

hence b in the Points of S2 by FUNCT_2:5; :: thesis: verum

end;assume b in the point-map of F .: K ; :: thesis: b in the Points of S2

then ex a being object st

( a in dom the point-map of F & a in K & b = the point-map of F . a ) by FUNCT_1:def 6;

hence b in the Points of S2 by FUNCT_2:5; :: thesis: verum