let F be ordered Field; :: thesis: for E being FieldExtension of F
for P being Ordering of F holds P c= QS (E,P)
let E be FieldExtension of F; :: thesis: for P being Ordering of F holds P c= QS (E,P)
let P be Ordering of F; :: thesis: P c= QS (E,P)
I: F is Subfield of E by FIELD_4:7;
then H: the carrier of F c= the carrier of E by EC_PF_1:def 1;

now :: thesis: for o being object st o in P holds
o in QS (E,P)

let o be object ; :: thesis: ( o in P implies o in QS (E,P) )
assume AS: o in P ; :: thesis: o in QS (E,P)
then reconsider a = o as Element of E by H;
reconsider f = <*a*> as non empty FinSequence of E ;
A: Sum f = a by RLVECT_1:44;
f is P -quadratic

proof

now :: thesis: for i being Element of NAT st i in dom f holds
ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) )

let i be Element of NAT ; :: thesis: ( i in dom f implies ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) )
assume B: i in dom f ; :: thesis: ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) )
dom f = {1} by FINSEQ_1:2, FINSEQ_1:38;
then C: i = 1 by B, TARSKI:def 1;
D: 1. F = 1. E by I, EC_PF_1:def 1;
thus ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) :: thesis: verum

proof

per cases ( a = 0. E or a <> 0. E ) ;

suppose a = 0. E ; :: thesis: ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) )

then (1. E) * ((0. E) ^2) = f . i by C;
hence ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) by D, REALALG1:25; :: thesis: verum

end;

suppose a <> 0. E ; :: thesis: ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) )

then ( not a is zero & a * ((1. E) ^2) = f . i ) by C;
hence ex c being non zero Element of E ex b being Element of E st
( c in P & f . i = c * (b ^2) ) by AS; :: thesis: verum

end;

end;

end;

end;

hence f is P -quadratic ; :: thesis: verum

end;

hence o in QS (E,P) by A; :: thesis: verum

end;

hence P c= QS (E,P) ; :: thesis: verum