let o be object ; :: thesis: for p being pair object holds Union (sqrtR (p,o)) = ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
let p be pair object ; :: thesis: Union (sqrtR (p,o)) = ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
defpred S1[ Nat] means (sqrtR (p,o)) . $1 c= ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))));
(sqrtR (p,o)) . 0 = R_ p by Th6;
then A1: S1[ 0 ] by XBOOLE_1:7, XBOOLE_1:10;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; :: thesis: S1[n + 1]
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (sqrtR (p,o)) . (n + 1) or a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) )
assume A4: a in (sqrtR (p,o)) . (n + 1) ; :: thesis: a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
(sqrtR (p,o)) . (n + 1) = (((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)))) \/ (sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n))) by Th8;
then ( a in ((sqrtR (p,o)) . n) \/ (sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n))) or a in sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) ) by XBOOLE_0:def 3, A4;
per cases then ( a in (sqrtR (p,o)) . n or a in sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)) or a in sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) ) by XBOOLE_0:def 3;
suppose a in (sqrtR (p,o)) . n ; :: thesis: a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A3; :: thesis: verum
end;
suppose A5: a in sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)) ; :: thesis: a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
(sqrtL (p,o)) . n c= Union (sqrtL (p,o)) by ABCMIZ_1:1;
then sqrt (o,((sqrtL (p,o)) . n),((sqrtL (p,o)) . n)) c= sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) by Th11;
then a in (R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o))))) by A5, XBOOLE_0:def 3;
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by XBOOLE_0:def 3; :: thesis: verum
end;
suppose A6: a in sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) ; :: thesis: a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
(sqrtR (p,o)) . n c= Union (sqrtR (p,o)) by ABCMIZ_1:1;
then sqrt (o,((sqrtR (p,o)) . n),((sqrtR (p,o)) . n)) c= sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) by Th11;
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A6, XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
A7: for n being Nat holds S1[n] from NAT_1:sch 2(A1, A2);
 thus Union (sqrtR (p,o)) c= ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) :: according to XBOOLE_0:def 10 :: thesis: ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) c= Union (sqrtR (p,o))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union (sqrtR (p,o)) or a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) )
assume a in Union (sqrtR (p,o)) ; :: thesis: a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))
then consider n being object such that
A8: ( n in dom (sqrtR (p,o)) & a in (sqrtR (p,o)) . n ) by CARD_5:2;
n in NAT by A8, Def5;
then reconsider n = n as Nat ;
(sqrtR (p,o)) . n c= ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A7;
hence a in ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) by A8; :: thesis: verum
end;
A9: sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) c= Union (sqrtR (p,o))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) or a in Union (sqrtR (p,o)) )
assume a in sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))) ; :: thesis: a in Union (sqrtR (p,o))
then consider x1, y1 being Surreal such that
A10: ( x1 in Union (sqrtL (p,o)) & y1 in Union (sqrtL (p,o)) & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
consider n being object such that
A11: ( n in dom (sqrtL (p,o)) & x1 in (sqrtL (p,o)) . n ) by A10, CARD_5:2;
consider m being object such that
A12: ( m in dom (sqrtL (p,o)) & y1 in (sqrtL (p,o)) . m ) by A10, CARD_5:2;
( n in NAT & m in NAT ) by A12, A11, Def4;
then reconsider n = n, m = m as Nat ;
set nm = n + m;
( m <= n + m & n <= n + m ) by NAT_1:11;
then ( (sqrtL (p,o)) . n c= (sqrtL (p,o)) . (n + m) & (sqrtL (p,o)) . m c= (sqrtL (p,o)) . (n + m) ) by Th7;
then a in sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m))) by A10, A11, A12, Def2;
then A13: a in ((sqrtR (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m)))) by XBOOLE_0:def 3;
(sqrtR (p,o)) . ((n + m) + 1) = (((sqrtR (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m))))) \/ (sqrt (o,((sqrtR (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m)))) by Th8;
then A14: a in (sqrtR (p,o)) . ((n + m) + 1) by A13, XBOOLE_0:def 3;
(n + m) + 1 in NAT ;
then (n + m) + 1 in dom (sqrtR (p,o)) by Def5;
hence a in Union (sqrtR (p,o)) by A14, CARD_5:2; :: thesis: verum
end;
A15: sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) c= Union (sqrtR (p,o))
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) or a in Union (sqrtR (p,o)) )
assume a in sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))) ; :: thesis: a in Union (sqrtR (p,o))
then consider x1, y1 being Surreal such that
A16: ( x1 in Union (sqrtR (p,o)) & y1 in Union (sqrtR (p,o)) & not x1 + y1 == 0_No & a = (o +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
consider n being object such that
A17: ( n in dom (sqrtR (p,o)) & x1 in (sqrtR (p,o)) . n ) by A16, CARD_5:2;
consider m being object such that
A18: ( m in dom (sqrtR (p,o)) & y1 in (sqrtR (p,o)) . m ) by A16, CARD_5:2;
( n in NAT & m in NAT ) by A18, A17, Def5;
then reconsider n = n, m = m as Nat ;
set nm = n + m;
( m <= n + m & n <= n + m ) by NAT_1:11;
then ( (sqrtR (p,o)) . n c= (sqrtR (p,o)) . (n + m) & (sqrtR (p,o)) . m c= (sqrtR (p,o)) . (n + m) ) by Th7;
then A19: a in sqrt (o,((sqrtR (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m))) by A16, A17, A18, Def2;
(sqrtR (p,o)) . ((n + m) + 1) = (((sqrtR (p,o)) . (n + m)) \/ (sqrt (o,((sqrtL (p,o)) . (n + m)),((sqrtL (p,o)) . (n + m))))) \/ (sqrt (o,((sqrtR (p,o)) . (n + m)),((sqrtR (p,o)) . (n + m)))) by Th8;
then A20: a in (sqrtR (p,o)) . ((n + m) + 1) by A19, XBOOLE_0:def 3;
(n + m) + 1 in NAT ;
then (n + m) + 1 in dom (sqrtR (p,o)) by Def5;
hence a in Union (sqrtR (p,o)) by A20, CARD_5:2; :: thesis: verum
end;
R_ p = (sqrtR (p,o)) . 0 by Th6;
then R_ p c= Union (sqrtR (p,o)) by ABCMIZ_1:1;
then (R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o))))) c= Union (sqrtR (p,o)) by A9, XBOOLE_1:8;
hence ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o))))) c= Union (sqrtR (p,o)) by XBOOLE_1:8, A15; :: thesis: verum