let a, b be Complex; :: thesis: ( 1 / a = b " implies a = b )
( 1 / a = 1 / b implies a = b ) by Th59;
hence ( 1 / a = b " implies a = b ) by Lm4; :: thesis: verum