let x be Surreal; :: thesis: x * 1_No = x
defpred S₁[ Ordinal] means for x being Surreal st born x c= $1 holds
x * 1_No = x;
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
let x be Surreal; :: thesis: ( born x c= D implies x * 1_No = x )
assume A3: born x c= D ; :: thesis: x * 1_No = x
A4: ( comp ((R_ x),x,1_No,(R_ 1_No)) = {} & comp ((L_ x),x,1_No,(R_ 1_No)) = {} ) by Th49;
A5: for X being surreal-membered set st X c= (L_ x) \/ (R_ x) holds
comp (X,x,1_No,(L_ 1_No)) = X

proof

let X be surreal-membered set ; :: thesis: ( X c= (L_ x) \/ (R_ x) implies comp (X,x,1_No,(L_ 1_No)) = X )
assume A6: X c= (L_ x) \/ (R_ x) ; :: thesis: comp (X,x,1_No,(L_ 1_No)) = X
thus comp (X,x,1_No,(L_ 1_No)) c= X :: according to XBOOLE_0:def 10 :: thesis: X c= comp (X,x,1_No,(L_ 1_No))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in comp (X,x,1_No,(L_ 1_No)) or o in X )
assume A7: o in comp (X,x,1_No,(L_ 1_No)) ; :: thesis: o in X
consider x1, y1 being Surreal such that
A8: ( o = ((x1 * 1_No) +' (x * y1)) +' (-' (x1 * y1)) & x1 in X & y1 in L_ 1_No ) by A7, Def14;
A9: y1 = 0_No by A8, TARSKI:def 1;
A10: born x1 in born x by A8, A6, SURREALO:1;
o = ((x1 * 1_No) + (x * y1)) + (- 0_No) by A8, A9, Th56
.= ((x1 * 1_No) + 0_No) + 0_No by A9, Th56
.= x1 * 1_No ;
hence o in X by A10, A2, A3, A8; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in X or o in comp (X,x,1_No,(L_ 1_No)) )
assume A11: o in X ; :: thesis: o in comp (X,x,1_No,(L_ 1_No))
reconsider x1 = o as Surreal by A11, SURREAL0:def 16;
A12: born x1 in born x by A11, A6, SURREALO:1;
0_No in L_ 1_No by TARSKI:def 1;
then A13: ((x1 * 1_No) + (x * 0_No)) + (- (x1 * 0_No)) in comp (X,x,1_No,(L_ 1_No)) by A11, Def14;
((x1 * 1_No) + (x * 0_No)) + (- (x1 * 0_No)) = ((x1 * 1_No) + (x * 0_No)) + (- 0_No) by Th56
.= ((x1 * 1_No) + 0_No) + 0_No by Th56
.= x1 * 1_No ;
hence o in comp (X,x,1_No,(L_ 1_No)) by A12, A2, A3, A13; :: thesis: verum

end;

A14: ( comp ((L_ x),x,1_No,(L_ 1_No)) = L_ x & comp ((R_ x),x,1_No,(L_ 1_No)) = R_ x ) by A5, XBOOLE_1:7;
x * 1_No = [((comp ((L_ x),x,1_No,(L_ 1_No))) \/ (comp ((R_ x),x,1_No,(R_ 1_No)))),((comp ((L_ x),x,1_No,(R_ 1_No))) \/ (comp ((R_ x),x,1_No,(L_ 1_No))))] by Th50
.= [(L_ x),(R_ x)] by A4, A14 ;
hence x * 1_No = x ; :: thesis: verum

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence x * 1_No = x ; :: thesis: verum