reconsider x = o as Surreal by A1;
take (No_sqrt_op (born x)) . x ; :: thesis: for x being Surreal st x = o holds
(No_sqrt_op (born x)) . x = (No_sqrt_op (born x)) . x
thus for x being Surreal st x = o holds
(No_sqrt_op (born x)) . x = (No_sqrt_op (born x)) . x ; :: thesis: verum