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
A1: ( f " is bijective & f " is open ) by Def4;
A2: f is bijective by Def4;
then A3: rng f = [#] S by FUNCT_2:def 3;
then (f ") " = f by A2, TOPS_2:51;
then A4: (f ") " is open by Def4;
(f ") " is bijective by A2, A3, TOPS_2:51;
hence f " is Collineation of S by A1, A4, Def4; :: thesis: verum