let T be TopStruct ; :: thesis: for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
let f be Homeomorphism of T; :: thesis: for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
set G = HomeoGroup T;
A1: dom f = [#] T by TOPS_2:def 5;
A2: f /" is Homeomorphism of T by Def4;
then reconsider g = f /" as Element of (HomeoGroup T) by Def5;
A3: rng f = [#] T by TOPS_2:def 5;
let a be Element of (HomeoGroup T); :: thesis: ( f = a implies a " = f /" )
assume A4: f = a ; :: thesis: a " = f /"
A5: g * a = f * (f /") by A4, A2, Def5
.= id T by A3, TOPS_2:52
.= 1_ (HomeoGroup T) by Th33 ;
a * g = (f /") * f by A4, A2, Def5
.= id T by A1, A3, TOPS_2:52
.= 1_ (HomeoGroup T) by Th33 ;
hence a " = f /" by A5, GROUP_1:5; :: thesis: verum