let x be set ; :: thesis: ( x tohilb is symmetric & dom (x tohilb) = rng (x tohilb) )
set g = x tohilb ;
per cases ( x <> {} or x = {} ) ;
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;
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;
end;