let s1, s2 be set ; :: thesis: ( ( for x being Surreal st x = o holds
s1 = (No_sqrt_op (born x)) . x ) & ( for x being Surreal st x = o holds
s2 = (No_sqrt_op (born x)) . x ) implies s1 = s2 )
assume that
A2: for x being Surreal st x = o holds
s1 = (No_sqrt_op (born x)) . x and
A3: for x being Surreal st x = o holds
s2 = (No_sqrt_op (born x)) . x ; :: thesis: s1 = s2
reconsider x = o as Surreal by A1;
s1 = (No_sqrt_op (born x)) . x by A2;
hence s1 = s2 by A3; :: thesis: verum