let x be set ; :: thesis: ( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )

set g = x tohilb ;

set g = x tohilb ;

per cases
( x <> {} or x = {} )
;

end;

suppose C00:
x <> {}
; :: thesis: ( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )

then C0:
x tohilb = id 1
by Lm18;

thus x tohilb is symmetric by C00; :: thesis: dom (x tohilb) = rng (x tohilb)

thus dom (x tohilb) = rng (x tohilb) by C0; :: thesis: verum

end;thus x tohilb is symmetric by C00; :: thesis: dom (x tohilb) = rng (x tohilb)

thus dom (x tohilb) = rng (x tohilb) by C0; :: thesis: verum

suppose C1:
x = {}
; :: thesis: ( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )

thus
x tohilb is symmetric
by C1, Lm17; :: thesis: dom (x tohilb) = rng (x tohilb)

( dom ((0,1) --> (1,0)) = {0,1} & rng ((0,1) --> (1,0)) = {0,1} ) by FUNCT_4:62, FUNCT_4:64;

hence dom (x tohilb) = rng (x tohilb) by C1, Lm17; :: thesis: verum

end;( dom ((0,1) --> (1,0)) = {0,1} & rng ((0,1) --> (1,0)) = {0,1} ) by FUNCT_4:62, FUNCT_4:64;

hence dom (x tohilb) = rng (x tohilb) by C1, Lm17; :: thesis: verum