let x be Surreal; :: thesis: for Inv being Function st x is positive & No_inverses_on ||.x.|| c= Inv holds
inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))]
let Inv be Function; :: thesis: ( x is positive & No_inverses_on ||.x.|| c= Inv implies inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))] )
set A = born x;
set Nx = ||.x.||;
assume A1: ( x is positive & No_inverses_on ||.x.|| c= Inv ) ; :: thesis: inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))]
consider S being c=-monotone Function-yielding Sequence such that
A2: ( dom S = succ (born x) & No_inverse_op (born x) = S . (born x) ) and
A3: for B being Ordinal st B in succ (born x) holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for o being object st o in Positives B holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | B)))))),(Union (divR (||.o.||,(union (rng (S | B))))))] ) ) by Def11;
consider SB being ManySortedSet of Positives (born x) such that
A4: S . (born x) = SB and
A5: for o being object st o in Positives (born x) holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | (born x))))))),(Union (divR (||.o.||,(union (rng (S | (born x)))))))] by A3, ORDINAL1:6;
set UA = union (rng (S | (born x)));
x in Day (born x) by SURREAL0:def 18;
then A6: x in Positives (born x) by A1, Def10;
set XX = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No};
A7: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x) by A1, Th24;
A8: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A1, Th20;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= dom (union (rng (S | (born x))))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} or o in dom (union (rng (S | (born x)))) )
assume A9: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: o in dom (union (rng (S | (born x))))
then reconsider o = o as Surreal by SURREAL0:def 16;
set b = born o;
A10: 0_No < o by A7, A9, Def10;
o in Day (born o) by SURREAL0:def 18;
then A11: o in Positives (born o) by A10, Def10;
A12: born o in born x by A9, A8, SURREALO:1;
born o in succ (born x) by ORDINAL1:8, A9, A8, SURREALO:1;
then ex SB being ManySortedSet of Positives (born o) st
( S . (born o) = SB & ( for o being object st o in Positives (born o) holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | (born o))))))),(Union (divR (||.o.||,(union (rng (S | (born o)))))))] ) ) by A3;
then o in dom (S . (born o)) by A11, PARTFUN1:def 2;
hence o in dom (union (rng (S | (born x)))) by A12, SURREALR:5; :: thesis: verum

end;

then A13: dom ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by RELAT_1:62;
( ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} = dom (No_inverses_on ||.x.||) & dom (No_inverses_on ||.x.||) c= dom Inv ) by RELAT_1:11, A1, Def13;
then A14: dom (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} by RELAT_1:62;
for a being object st a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a

proof

let a be object ; :: thesis: ( a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} implies ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a )
assume A15: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a
then reconsider o = a as Surreal by SURREAL0:def 16;
A16: ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (union (rng (S | (born x)))) . a by A15, FUNCT_1:49;
set b = born o;
A17: 0_No < o by A7, A15, Def10;
o in Day (born o) by SURREAL0:def 18;
then A18: o in Positives (born o) by A17, Def10;
A19: born o in born x by A15, A8, SURREALO:1;
A20: born o in succ (born x) by ORDINAL1:8, A15, A8, SURREALO:1;
then ex SB being ManySortedSet of Positives (born o) st
( S . (born o) = SB & ( for o being object st o in Positives (born o) holds
SB . o = [(Union (divL (||.o.||,(union (rng (S | (born o))))))),(Union (divR (||.o.||,(union (rng (S | (born o)))))))] ) ) by A3;
then A21: o in dom (S . (born o)) by A18, PARTFUN1:def 2;
then A22: (union (rng (S | (born x)))) . o = (union (rng S)) . o by A19, SURREALR:5;
A23: born o in dom S by ORDINAL1:8, A15, A8, SURREALO:1, A2;
A24: No_inverse_op (born o) = S . (born o) by A2, A3, Th25, A20;
A25: (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . o = Inv . o by A15, FUNCT_1:49;
A26: o in dom (No_inverses_on ||.x.||) by A15, Def13;
(No_inverses_on ||.x.||) . o = inv o by A15, Def13;
then [o,(inv o)] in No_inverses_on ||.x.|| by A26, FUNCT_1:1;
then (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . o = inv o by A1, A25, FUNCT_1:1;
hence ((union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a by A24, A16, A22, A21, A23, SURREALR:2; :: thesis: verum

end;

then (union (rng (S | (born x)))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) = Inv | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) by A13, A14, FUNCT_1:2;
then ( divL (||.x.||,(union (rng (S | (born x))))) = divL (||.x.||,Inv) & divR (||.x.||,(union (rng (S | (born x))))) = divR (||.x.||,Inv) ) by Th17;
hence inv x = [(Union (divL (||.x.||,Inv))),(Union (divR (||.x.||,Inv)))] by A6, A4, A5, A2; :: thesis: verum