let x be Surreal; :: thesis: ( 0_No < x implies (sqrt x) " == sqrt (x ") )
assume A1: 0_No < x ; :: thesis: (sqrt x) " == sqrt (x ")
then reconsider a = x as positive Surreal by SURREALI:def 8;
set S = sqrt a;
set T = sqrt (a ");
A2: ( not sqrt a == 0_No & not sqrt (a ") == 0_No ) by SURREALI:def 8;
A3: 0_No <= a " by SURREALI:def 8;
0_No <= x by A1;
then ( ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == a * ((sqrt (a ")) * (sqrt (a "))) & a * ((sqrt (a ")) * (sqrt (a "))) == a * (a ") ) by A3, Th21, SURREALR:54;
then A4: ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == a * (a ") by SURREALO:4;
not a == 0_No by A1;
then a * (a ") == 1_No by SURREALI:33;
then A5: ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == 1_No by A4, SURREALO:4;
A6: 0_No <= 1_No by SURREALI:def 8;
A7: - 1_No <= - 0_No by SURREALR:10, SURREALI:def 8;
( ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == (((sqrt a) * (sqrt a)) * (sqrt (a "))) * (sqrt (a ")) & (((sqrt a) * (sqrt a)) * (sqrt (a "))) * (sqrt (a ")) == ((sqrt a) * ((sqrt a) * (sqrt (a ")))) * (sqrt (a ")) ) by SURREALR:69, SURREALR:54;
then ( ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == ((sqrt a) * ((sqrt a) * (sqrt (a ")))) * (sqrt (a ")) & ((sqrt a) * ((sqrt a) * (sqrt (a ")))) * (sqrt (a ")) == ((sqrt a) * (sqrt (a "))) * ((sqrt a) * (sqrt (a "))) ) by SURREALO:4, SURREALR:69;
then ((sqrt a) * (sqrt a)) * ((sqrt (a ")) * (sqrt (a "))) == ((sqrt a) * (sqrt (a "))) * ((sqrt a) * (sqrt (a "))) by SURREALO:4;
then ((sqrt a) * (sqrt (a "))) * ((sqrt a) * (sqrt (a "))) == 1_No by A5, SURREALO:4;
then ( (sqrt a) * (sqrt (a ")) == sqrt 1_No or (sqrt a) * (sqrt (a ")) == - (sqrt 1_No) ) by A6, Th28;
hence (sqrt x) " == sqrt (x ") by A2, A7, SURREALI:def 8, SURREALI:42, SURREALO:4; :: thesis: verum