the point-map of F " K c= the Points of S1

proof

hence
the point-map of F " K is Subset of the Points of S1
; :: 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 S1 )

assume b in the point-map of F " K ; :: thesis: b in the Points of S1

then b in dom the point-map of F by FUNCT_1:def 7;

hence b in the Points of S1 ; :: thesis: verum

end;assume b in the point-map of F " K ; :: thesis: b in the Points of S1

then b in dom the point-map of F by FUNCT_1:def 7;

hence b in the Points of S1 ; :: thesis: verum