let mym, myp be Element of REAL ; :: thesis:
assume A: ( mym = 1 & myp = - 1 ) ; :: thesis:
for x being object holds
( x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) iff x in RAT )

proof

let x be object ; :: thesis:
B1: ( x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) implies x in RAT )

proof

assume x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose x in Union (GoCross_Union mym) ; :: thesis:

then consider k being Nat such that
D1: x in (GoCross_Union mym) . k by PROB_1:12;

per cases ;

suppose k = 0 ; :: thesis:

then x in Union (GoCross_Partial_Union (mym,0)) by D1, Def6;
then consider k2 being Nat such that
E1: x in (GoCross_Partial_Union (mym,0)) . k2 by PROB_1:12;

per cases ;

suppose k2 = 0 ; :: thesis:

then x in (GoCross_Seq_REAL (mym,0)) . 0 by E1, Def5;
then x in {((mym * 0) * ((0 + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

suppose k2 > 0 ; :: thesis:

then consider n being Nat such that
H1: k2 = n + 1 by NAT_1:6;
x in ((GoCross_Partial_Union (mym,0)) . n) \/ ((GoCross_Seq_REAL (mym,0)) . (n + 1)) by E1, H1, Def5;

per cases by XBOOLE_0:def 3;

suppose H1: x in (GoCross_Partial_Union (mym,0)) . n ; :: thesis:

defpred S₁[ Nat] means ( x in (GoCross_Partial_Union (mym,0)) . $1 implies x in RAT );
x in RAT

proof

J0: S₁[ 0 ]

proof

assume x in (GoCross_Partial_Union (mym,0)) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (mym,0)) . 0 by Def5;
then x in {((mym * 0) * ((0 + 1) "))} by Def4;
then x = 0 by TARSKI:def 1;
hence x in RAT by NUMBERS:18; :: thesis:

end;

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume K1: S₁[n] ; :: thesis:
assume x in (GoCross_Partial_Union (mym,0)) . (n + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (mym,0)) . n) \/ ((GoCross_Seq_REAL (mym,0)) . (n + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (mym,0)) . n ; :: thesis:

hence x in RAT by K1; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (mym,0)) . (n + 1) ; :: thesis:

then x in {((mym * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence x in RAT by H1; :: thesis:

end;

hence x in RAT ; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (mym,0)) . (n + 1) ; :: thesis:

then x in {((mym * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

end;

end;

suppose k > 0 ; :: thesis:

then consider kh being Nat such that
H1: k = kh + 1 by NAT_1:6;
x in ((GoCross_Union mym) . kh) \/ (Union (GoCross_Partial_Union (mym,(kh + 1)))) by D1, H1, Def6;

per cases by XBOOLE_0:def 3;

suppose J00: x in (GoCross_Union mym) . kh ; :: thesis:

defpred S₁[ Nat] means ( x in (GoCross_Union mym) . $1 implies x in RAT );
J0: S₁[ 0 ]

proof

assume x in (GoCross_Union mym) . 0 ; :: thesis:
then x in Union (GoCross_Partial_Union (mym,0)) by Def6;
then consider k2 being Nat such that
E1: x in (GoCross_Partial_Union (mym,0)) . k2 by PROB_1:12;

per cases ;

suppose k2 = 0 ; :: thesis:

then x in (GoCross_Seq_REAL (mym,0)) . 0 by E1, Def5;
then x in {((mym * 0) * ((0 + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

suppose k2 > 0 ; :: thesis:

then consider n being Nat such that
H1: k2 = n + 1 by NAT_1:6;
x in ((GoCross_Partial_Union (mym,0)) . n) \/ ((GoCross_Seq_REAL (mym,0)) . (n + 1)) by E1, H1, Def5;

per cases by XBOOLE_0:def 3;

suppose H1: x in (GoCross_Partial_Union (mym,0)) . n ; :: thesis:

defpred S₂[ Nat] means ( x in (GoCross_Partial_Union (mym,0)) . $1 implies x in RAT );
J0: S₂[ 0 ]

proof

assume x in (GoCross_Partial_Union (mym,0)) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (mym,0)) . 0 by Def5;
then x in {((mym * 0) * ((0 + 1) "))} by Def4;
then x = 0 by TARSKI:def 1;
hence x in RAT by NUMBERS:18; :: thesis:

end;

J1: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume K1: S₂[n] ; :: thesis:
assume x in (GoCross_Partial_Union (mym,0)) . (n + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (mym,0)) . n) \/ ((GoCross_Seq_REAL (mym,0)) . (n + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (mym,0)) . n ; :: thesis:

hence x in RAT by K1; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (mym,0)) . (n + 1) ; :: thesis:

then x in {((mym * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(J0, J1);
hence x in RAT by H1; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (mym,0)) . (n + 1) ; :: thesis:

then x in {((mym * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

end;

end;

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume K0000: S₁[n] ; :: thesis:
( x in (GoCross_Union mym) . (n + 1) implies x in RAT )

proof

assume x in (GoCross_Union mym) . (n + 1) ; :: thesis:
then x in ((GoCross_Union mym) . n) \/ (Union (GoCross_Partial_Union (mym,(n + 1)))) by Def6;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Union mym) . n ; :: thesis:

hence x in RAT by K0000; :: thesis:

end;

suppose x in Union (GoCross_Partial_Union (mym,(n + 1))) ; :: thesis:

then consider k being Nat such that
H1: x in (GoCross_Partial_Union (mym,(n + 1))) . k by PROB_1:12;
defpred S₂[ Nat] means ( x in (GoCross_Partial_Union (mym,(n + 1))) . $1 implies x in RAT );
J0: S₂[ 0 ]

proof

assume x in (GoCross_Partial_Union (mym,(n + 1))) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (mym,(n + 1))) . 0 by Def5;
then x in {((mym * (n + 1)) * ((0 + 1) "))} by Def4;
then x = 1 * (n + 1) by TARSKI:def 1, A;
hence x in RAT by NUMBERS:17, NUMBERS:14; :: thesis:

end;

J1: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume K0: S₂[k] ; :: thesis:
set o = n + 1;
set o2 = k + 2;
set o3 = k + 1;
( x in (GoCross_Partial_Union (mym,(n + 1))) . (k + 1) implies x in RAT )

proof

assume x in (GoCross_Partial_Union (mym,(n + 1))) . (k + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (mym,(n + 1))) . k) \/ ((GoCross_Seq_REAL (mym,(n + 1))) . (k + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (mym,(n + 1))) . k ; :: thesis:

hence x in RAT by K0; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (mym,(n + 1))) . (k + 1) ; :: thesis:

then x in {((mym * (n + 1)) * (((k + 1) + 1) "))} by Def4;
then OZ: x = (n + 1) * ((k + 2) ") by TARSKI:def 1, A;
reconsider o2 = k + 2, o = n + 1 as Element of INT by NUMBERS:17;
o / o2 is Element of RAT by RAT_1:def 1;
hence x in RAT by OZ; :: thesis:

end;

end;

end;

hence S₂[k + 1] ; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(J0, J1);
hence x in RAT by H1; :: thesis:

end;

end;

end;

hence S₁[n + 1] ; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence x in RAT by J00; :: thesis:

end;

suppose x in Union (GoCross_Partial_Union (mym,(kh + 1))) ; :: thesis:

then consider q being Nat such that
JK0: x in (GoCross_Partial_Union (mym,(kh + 1))) . q by PROB_1:12;
defpred S₁[ Nat] means ( x in (GoCross_Partial_Union (mym,(kh + 1))) . $1 implies x in RAT );
J0: S₁[ 0 ]

proof

assume x in (GoCross_Partial_Union (mym,(kh + 1))) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (mym,(kh + 1))) . 0 by Def5;
then x in {((mym * (kh + 1)) * ((0 + 1) "))} by Def4;
then x = (mym * (kh + 1)) * (1 ") by TARSKI:def 1;
hence x in RAT by A, NUMBERS:17, NUMBERS:14; :: thesis:

end;

J1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume K0: S₁[k] ; :: thesis:
set o = kh + 1;
set o2 = k + 2;
set o3 = k + 1;
( x in (GoCross_Partial_Union (mym,(kh + 1))) . (k + 1) implies x in RAT )

proof

assume x in (GoCross_Partial_Union (mym,(kh + 1))) . (k + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (mym,(kh + 1))) . k) \/ ((GoCross_Seq_REAL (mym,(kh + 1))) . (k + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (mym,(kh + 1))) . k ; :: thesis:

hence x in RAT by K0; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (mym,(kh + 1))) . (k + 1) ; :: thesis:

then x in {((mym * (kh + 1)) * (((k + 1) + 1) "))} by Def4;
then OZ: x = (kh + 1) * ((k + 2) ") by TARSKI:def 1, A;
reconsider o2 = k + 2, o = kh + 1 as Element of INT by NUMBERS:17;
o / o2 is Element of RAT by RAT_1:def 1;
hence x in RAT by OZ; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(J0, J1);
hence x in RAT by JK0; :: thesis:

end;

end;

end;

end;

end;

suppose x in Union (GoCross_Union myp) ; :: thesis:

then consider k being Nat such that
D1: x in (GoCross_Union myp) . k by PROB_1:12;

per cases ;

suppose k = 0 ; :: thesis:

then x in Union (GoCross_Partial_Union (myp,0)) by D1, Def6;
then consider k2 being Nat such that
E1: x in (GoCross_Partial_Union (myp,0)) . k2 by PROB_1:12;

per cases ;

suppose k2 = 0 ; :: thesis:

then x in (GoCross_Seq_REAL (myp,0)) . 0 by E1, Def5;
then x in {((myp * 0) * ((0 + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

suppose k2 > 0 ; :: thesis:

then consider n being Nat such that
H1: k2 = n + 1 by NAT_1:6;
x in ((GoCross_Partial_Union (myp,0)) . n) \/ ((GoCross_Seq_REAL (myp,0)) . (n + 1)) by E1, H1, Def5;

per cases by XBOOLE_0:def 3;

suppose H1: x in (GoCross_Partial_Union (myp,0)) . n ; :: thesis:

defpred S₁[ Nat] means ( x in (GoCross_Partial_Union (myp,0)) . $1 implies x in RAT );
J0: S₁[ 0 ]

proof

assume x in (GoCross_Partial_Union (myp,0)) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (myp,0)) . 0 by Def5;
then x in {((myp * 0) * ((0 + 1) "))} by Def4;
then x = 0 by TARSKI:def 1;
hence x in RAT by NUMBERS:18; :: thesis:

end;

x in RAT

proof

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume K1: S₁[n] ; :: thesis:
assume x in (GoCross_Partial_Union (myp,0)) . (n + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (myp,0)) . n) \/ ((GoCross_Seq_REAL (myp,0)) . (n + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (myp,0)) . n ; :: thesis:

hence x in RAT by K1; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (myp,0)) . (n + 1) ; :: thesis:

then x in {((myp * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence x in RAT by H1; :: thesis:

end;

hence x in RAT ; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (myp,0)) . (n + 1) ; :: thesis:

then x in {((myp * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

end;

end;

suppose k > 0 ; :: thesis:

then consider kh being Nat such that
H1: k = kh + 1 by NAT_1:6;
x in ((GoCross_Union myp) . kh) \/ (Union (GoCross_Partial_Union (myp,(kh + 1)))) by D1, H1, Def6;

per cases by XBOOLE_0:def 3;

suppose J00: x in (GoCross_Union myp) . kh ; :: thesis:

defpred S₁[ Nat] means ( x in (GoCross_Union myp) . $1 implies x in RAT );
J0: S₁[ 0 ]

proof

assume x in (GoCross_Union myp) . 0 ; :: thesis:
then x in Union (GoCross_Partial_Union (myp,0)) by Def6;
then consider k2 being Nat such that
E1: x in (GoCross_Partial_Union (myp,0)) . k2 by PROB_1:12;

per cases ;

suppose k2 = 0 ; :: thesis:

then x in (GoCross_Seq_REAL (myp,0)) . 0 by E1, Def5;
then x in {((myp * 0) * ((0 + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

suppose k2 > 0 ; :: thesis:

then consider n being Nat such that
H1: k2 = n + 1 by NAT_1:6;
x in ((GoCross_Partial_Union (myp,0)) . n) \/ ((GoCross_Seq_REAL (myp,0)) . (n + 1)) by E1, H1, Def5;

per cases by XBOOLE_0:def 3;

suppose H1: x in (GoCross_Partial_Union (myp,0)) . n ; :: thesis:

x in RAT

proof

defpred S₂[ Nat] means ( x in (GoCross_Partial_Union (myp,0)) . $1 implies x in RAT );
J0: S₂[ 0 ]

proof

assume x in (GoCross_Partial_Union (myp,0)) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (myp,0)) . 0 by Def5;
then x in {((myp * 0) * ((0 + 1) "))} by Def4;
then x = 0 by TARSKI:def 1;
hence x in RAT by NUMBERS:18; :: thesis:

end;

J1: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume K1: S₂[n] ; :: thesis:
assume x in (GoCross_Partial_Union (myp,0)) . (n + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (myp,0)) . n) \/ ((GoCross_Seq_REAL (myp,0)) . (n + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (myp,0)) . n ; :: thesis:

hence x in RAT by K1; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (myp,0)) . (n + 1) ; :: thesis:

then x in {((myp * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

for n being Nat holds S₂[n] from NAT_1:sch 2(J0, J1);
hence x in RAT by H1; :: thesis:

end;

hence x in RAT ; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (myp,0)) . (n + 1) ; :: thesis:

then x in {((myp * 0) * (((n + 1) + 1) "))} by Def4;
then x in INT by INT_1:def 1;
hence x in RAT by NUMBERS:14; :: thesis:

end;

end;

end;

end;

end;

J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume K0000: S₁[n] ; :: thesis:
( x in (GoCross_Union myp) . (n + 1) implies x in RAT )

proof

assume x in (GoCross_Union myp) . (n + 1) ; :: thesis:
then x in ((GoCross_Union myp) . n) \/ (Union (GoCross_Partial_Union (myp,(n + 1)))) by Def6;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Union myp) . n ; :: thesis:

hence x in RAT by K0000; :: thesis:

end;

suppose x in Union (GoCross_Partial_Union (myp,(n + 1))) ; :: thesis:

then consider k being Nat such that
H1: x in (GoCross_Partial_Union (myp,(n + 1))) . k by PROB_1:12;
defpred S₂[ Nat] means ( x in (GoCross_Partial_Union (myp,(n + 1))) . $1 implies x in RAT );
J0: S₂[ 0 ]

proof

assume x in (GoCross_Partial_Union (myp,(n + 1))) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (myp,(n + 1))) . 0 by Def5;
then x in {((myp * (n + 1)) * ((0 + 1) "))} by Def4;
then HH: x = - (1 * (n + 1)) by TARSKI:def 1, A;
- (n + 1) is Element of INT by INT_1:def 1;
hence x in RAT by HH, NUMBERS:14; :: thesis:

end;

J1: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume K0: S₂[k] ; :: thesis:
( x in (GoCross_Partial_Union (myp,(n + 1))) . (k + 1) implies x in RAT )

proof

assume x in (GoCross_Partial_Union (myp,(n + 1))) . (k + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (myp,(n + 1))) . k) \/ ((GoCross_Seq_REAL (myp,(n + 1))) . (k + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (myp,(n + 1))) . k ; :: thesis:

hence x in RAT by K0; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (myp,(n + 1))) . (k + 1) ; :: thesis:

then x in {((myp * (n + 1)) * (((k + 1) + 1) "))} by Def4;
hence x in RAT by A, RAT_1:def 2; :: thesis:

end;

end;

end;

hence S₂[k + 1] ; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(J0, J1);
hence x in RAT by H1; :: thesis:

end;

end;

end;

hence S₁[n + 1] ; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence x in RAT by J00; :: thesis:

end;

suppose x in Union (GoCross_Partial_Union (myp,(kh + 1))) ; :: thesis:

then consider q being Nat such that
JK0: x in (GoCross_Partial_Union (myp,(kh + 1))) . q by PROB_1:12;
defpred S₁[ Nat] means ( x in (GoCross_Partial_Union (myp,(kh + 1))) . $1 implies x in RAT );
J0: S₁[ 0 ]

proof

assume x in (GoCross_Partial_Union (myp,(kh + 1))) . 0 ; :: thesis:
then x in (GoCross_Seq_REAL (myp,(kh + 1))) . 0 by Def5;
then x in {((myp * (kh + 1)) * ((0 + 1) "))} by Def4;
then HH: x = - (kh + 1) by TARSKI:def 1, A;
- (kh + 1) in INT by INT_1:def 1;
hence x in RAT by HH, NUMBERS:14; :: thesis:

end;

J1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume K0: S₁[k] ; :: thesis:
set o3 = k + 1;
( x in (GoCross_Partial_Union (myp,(kh + 1))) . (k + 1) implies x in RAT )

proof

assume x in (GoCross_Partial_Union (myp,(kh + 1))) . (k + 1) ; :: thesis:
then x in ((GoCross_Partial_Union (myp,(kh + 1))) . k) \/ ((GoCross_Seq_REAL (myp,(kh + 1))) . (k + 1)) by Def5;

per cases by XBOOLE_0:def 3;

suppose x in (GoCross_Partial_Union (myp,(kh + 1))) . k ; :: thesis:

hence x in RAT by K0; :: thesis:

end;

suppose x in (GoCross_Seq_REAL (myp,(kh + 1))) . (k + 1) ; :: thesis:

then x in {((myp * (kh + 1)) * (((k + 1) + 1) "))} by Def4;
hence x in RAT by A, RAT_1:def 2; :: thesis:

end;

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(J0, J1);
hence x in RAT by JK0; :: thesis:

end;

end;

end;

end;

end;

end;

end;

( x in RAT implies x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) )

proof

assume x in RAT ; :: thesis:
then reconsider x = x as Rational ;
consider m being Integer, k being Nat such that
C0: ( k > 0 & x = m / k ) by RAT_1:8;
consider m2 being Nat such that
C2: ( m = m2 or m = - m2 ) by INT_1:2;

per cases by C2;

suppose S1: m = m2 ; :: thesis:

consider q2 being Nat such that
F2: q2 = k - 1 by C0;
G1: x in (GoCross_Seq_REAL (mym,m2)) . q2

proof

(GoCross_Seq_REAL (mym,m2)) . q2 = {((1 * m2) * ((q2 + 1) "))} by Def4, A;
hence x in (GoCross_Seq_REAL (mym,m2)) . q2 by C0, S1, F2, TARSKI:def 1; :: thesis:

end;

G2: x in (GoCross_Partial_Union (mym,m2)) . q2

proof

per cases ;

suppose q2 = 0 ; :: thesis:

hence x in (GoCross_Partial_Union (mym,m2)) . q2 by Def5, G1; :: thesis:

end;

suppose q2 > 0 ; :: thesis:

then consider q3 being Nat such that
F2: q3 = q2 - 1 ;
x in (GoCross_Partial_Union (mym,m2)) . q2

proof

(GoCross_Partial_Union (mym,m2)) . (q3 + 1) = ((GoCross_Partial_Union (mym,m2)) . q3) \/ ((GoCross_Seq_REAL (mym,m2)) . (q3 + 1)) by Def5;
hence x in (GoCross_Partial_Union (mym,m2)) . q2 by F2, G1, XBOOLE_0:def 3; :: thesis:

end;

hence x in (GoCross_Partial_Union (mym,m2)) . q2 ; :: thesis:

end;

end;

end;

x in (GoCross_Union mym) . m2

proof

per cases ;

suppose I1: m2 = 0 ; :: thesis:

x in Union (GoCross_Partial_Union (mym,m2)) by G2, PROB_1:12;
hence x in (GoCross_Union mym) . m2 by I1, Def6; :: thesis:

end;

suppose m2 > 0 ; :: thesis:

then consider m3 being Nat such that
F2: m3 = m2 - 1 ;
I2: ( x in (GoCross_Union mym) . m3 or x in Union (GoCross_Partial_Union (mym,(m3 + 1))) ) by F2, G2, PROB_1:12;
x in (GoCross_Union mym) . m2

proof

(GoCross_Union mym) . (m3 + 1) = ((GoCross_Union mym) . m3) \/ (Union (GoCross_Partial_Union (mym,(m3 + 1)))) by Def6;
hence x in (GoCross_Union mym) . m2 by I2, XBOOLE_0:def 3, F2; :: thesis:

end;

hence x in (GoCross_Union mym) . m2 ; :: thesis:

end;

end;

end;

then x in Union (GoCross_Union mym) by PROB_1:12;
hence x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) by XBOOLE_0:def 3; :: thesis:

end;

suppose S1: m = - m2 ; :: thesis:

consider q2 being Nat such that
F2: q2 = k - 1 by C0;
G1: x in (GoCross_Seq_REAL (myp,m2)) . q2

proof

(GoCross_Seq_REAL (myp,m2)) . q2 = {(((- 1) * m2) * ((q2 + 1) "))} by Def4, A;
hence x in (GoCross_Seq_REAL (myp,m2)) . q2 by C0, S1, F2, TARSKI:def 1; :: thesis:

end;

G2: x in (GoCross_Partial_Union (myp,m2)) . q2

proof

per cases ;

suppose q2 = 0 ; :: thesis:

hence x in (GoCross_Partial_Union (myp,m2)) . q2 by Def5, G1; :: thesis:

end;

suppose q2 > 0 ; :: thesis:

then consider q3 being Nat such that
F2: q3 = q2 - 1 ;
x in (GoCross_Partial_Union (myp,m2)) . q2

proof

(GoCross_Partial_Union (myp,m2)) . (q3 + 1) = ((GoCross_Partial_Union (myp,m2)) . q3) \/ ((GoCross_Seq_REAL (myp,m2)) . (q3 + 1)) by Def5;
hence x in (GoCross_Partial_Union (myp,m2)) . q2 by F2, G1, XBOOLE_0:def 3; :: thesis:

end;

hence x in (GoCross_Partial_Union (myp,m2)) . q2 ; :: thesis:

end;

end;

end;

x in (GoCross_Union myp) . m2

proof

per cases ;

suppose m2 = 0 ; :: thesis:

then (GoCross_Union myp) . m2 = Union (GoCross_Partial_Union (myp,m2)) by Def6;
hence x in (GoCross_Union myp) . m2 by G2, PROB_1:12; :: thesis:

end;

suppose m2 > 0 ; :: thesis:

then consider m3 being Nat such that
F2: m3 = m2 - 1 ;
I2: ( x in (GoCross_Union myp) . m3 or x in Union (GoCross_Partial_Union (myp,(m3 + 1))) ) by F2, G2, PROB_1:12;
x in (GoCross_Union myp) . m2

proof

(GoCross_Union myp) . (m3 + 1) = ((GoCross_Union myp) . m3) \/ (Union (GoCross_Partial_Union (myp,(m3 + 1)))) by Def6;
hence x in (GoCross_Union myp) . m2 by I2, XBOOLE_0:def 3, F2; :: thesis:

end;

hence x in (GoCross_Union myp) . m2 ; :: thesis:

end;

end;

end;

then ( x in Union (GoCross_Union mym) or x in Union (GoCross_Union myp) ) by PROB_1:12;
hence x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence ( x in (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) iff x in RAT ) by B1; :: thesis:

end;

hence (Union (GoCross_Union mym)) \/ (Union (GoCross_Union myp)) = RAT ; :: thesis: