let S be non empty TopStruct ; :: thesis: for f being Collineation of S holds f " is Collineation of S
let f be Collineation of S; :: thesis: f " is Collineation of S
f is bijective by Def4;
then A1: ( f is one-to-one & f is onto ) ;
then A2: rng f = [#] S by FUNCT_2:def 3;
f " is isomorphic

proof

thus ( f " is bijective & f " is open ) by Def4; :: according to PENCIL_2:def 4 :: thesis: ( (f " ) " is bijective & (f " ) " is open )
(f " ) " = f by A1, A2, TOPS_2:64;
hence ( (f " ) " is bijective & (f " ) " is open ) by Def4; :: thesis: verum

end;

hence f " is Collineation of S ; :: thesis: verum