let F be ordered Field; :: thesis: for E being ordered FieldExtension of F
for P being Ordering of F
for O being Ordering of E holds
( O extends P iff (signum O) | the carrier of F = signum P )
let E be ordered FieldExtension of F; :: thesis: for P being Ordering of F
for O being Ordering of E holds
( O extends P iff (signum O) | the carrier of F = signum P )
let P be Ordering of F; :: thesis: for O being Ordering of E holds
( O extends P iff (signum O) | the carrier of F = signum P )
let O be Ordering of E; :: thesis: ( O extends P iff (signum O) | the carrier of F = signum P )
set sP = signum P;
set sO = signum O;
H: ( F is Subfield of E & P \/ (- P) = the carrier of F ) by REALALG1:def 15, FIELD_4:7;
then I: the carrier of F c= the carrier of E by EC_PF_1:def 1;
C: (dom (signum O)) /\ the carrier of F = the carrier of E /\ the carrier of F by FUNCT_2:def 1
.= the carrier of F by I, XBOOLE_1:28
.= dom (signum P) by FUNCT_2:def 1 ;

A: now :: thesis: ( O extends P implies (signum O) | the carrier of F = signum P )

assume B: O extends P ; :: thesis: (signum O) | the carrier of F = signum P

now :: thesis: for x being object st x in dom (signum P) holds
(signum O) . x = (signum P) . x

let x be object ; :: thesis: ( x in dom (signum P) implies (signum O) . b₁ = (signum P) . b₁ )
assume x in dom (signum P) ; :: thesis: (signum O) . b₁ = (signum P) . b₁
then reconsider a = x as Element of F by FUNCT_2:def 1;
reconsider b = a as Element of E by I;

per cases ( x in P \ {(0. F)} or x = 0. F or ( not x in P \ {(0. F)} & x <> 0. F ) ) ;

suppose E: x in P \ {(0. F)} ; :: thesis: (signum O) . b₁ = (signum P) . b₁

then ( a in P & not a in {(0. F)} ) by XBOOLE_0:def 5;
then ( a in O & not a in {(0. E)} ) by B, H, XBOOLE_0:def 4, EC_PF_1:def 1;
then F: x in O \ {(0. E)} by XBOOLE_0:def 5;
thus (signum O) . x = signum (O,b) by sgnF
.= 1 by F, defsgn
.= signum (P,a) by E, defsgn
.= (signum P) . x by sgnF ; :: thesis: verum

end;

suppose E: x = 0. F ; :: thesis: (signum O) . b₁ = (signum P) . b₁

then F: x = 0. E by H, EC_PF_1:def 1;
thus (signum O) . x = signum (O,b) by sgnF
.= 0 by F, defsgn
.= signum (P,a) by E, defsgn
.= (signum P) . x by sgnF ; :: thesis: verum

end;

suppose E: ( not x in P \ {(0. F)} & x <> 0. F ) ; :: thesis: (signum O) . b₁ = (signum P) . b₁

then ( not a in P or a in {(0. F)} ) by XBOOLE_0:def 5;
then not a in O by B, XBOOLE_0:def 4, E, TARSKI:def 1;
then F: ( not x in O \ {(0. E)} & x <> 0. E ) by H, E, EC_PF_1:def 1, XBOOLE_0:def 5;
thus (signum O) . x = signum (O,b) by sgnF
.= - 1 by F, defsgn
.= signum (P,a) by E, defsgn
.= (signum P) . x by sgnF ; :: thesis: verum

end;

end;

end;

hence (signum O) | the carrier of F = signum P by C, FUNCT_1:46; :: thesis: verum

end;

now :: thesis: ( (signum O) | the carrier of F = signum P implies O extends P )

assume A: (signum O) | the carrier of F = signum P ; :: thesis: O extends P

now :: thesis: for x being object st x in P holds
x in O

let x be object ; :: thesis: ( x in P implies b₁ in O )
assume B: x in P ; :: thesis: b₁ in O

per cases ( x <> 0. F or x = 0. F ) ;

suppose x <> 0. F ; :: thesis: b₁ in O

then not x in {(0. F)} by TARSKI:def 1;
then D: x in P \ {(0. F)} by B, XBOOLE_0:def 5;
reconsider a = x as Element of F by B;
reconsider b = a as Element of E by I;
E: dom (signum P) = the carrier of F by FUNCT_2:def 1;
signum (O,b) = (signum O) . b by sgnF
.= (signum P) . a by C, E, A, FUNCT_1:48
.= signum (P,a) by sgnF
.= 1 by D, defsgn ;
then b in O \ {(0. E)} by defsgn;
hence x in O by XBOOLE_0:def 5; :: thesis: verum

end;

suppose x = 0. F ; :: thesis: b₁ in O

then x = 0. E by H, EC_PF_1:def 1;
hence x in O by REALALG1:25; :: thesis: verum

end;

end;

end;

then P c= O ;
hence O extends P by l13; :: thesis: verum

end;

hence ( O extends P iff (signum O) | the carrier of F = signum P ) by A; :: thesis: verum