let T be TopStruct ; :: thesis: id T = 1_ (HomeoGroup T)
set G = HomeoGroup T;
reconsider e = id T as Element of (HomeoGroup T) by Def5;

now :: thesis: for h being Element of (HomeoGroup T) holds
( h * e = h & e * h = h )

let h be Element of (HomeoGroup T); :: thesis: ( h * e = h & e * h = h )
reconsider h1 = h as Homeomorphism of T by Def5;
thus h * e = (id T) * h1 by Def5
.= h by FUNCT_2:17 ; :: thesis: e * h = h
thus e * h = h1 * (id T) by Def5
.= h by FUNCT_2:17 ; :: thesis: verum

end;

hence id T = 1_ (HomeoGroup T) by GROUP_1:4; :: thesis: verum