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

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