let R be non degenerated preordered Ring; :: thesis: Char R = 0
set P = the Preordering of R;
A: 1. R in the Preordering of R by ord3;
B: QS R c= the Preordering of R by ord2;
set n = Char R;
now :: thesis: not Char R <> 0
assume AS: Char R <> 0 ; :: thesis: contradiction
then C: (Char R) '*' (1. R) = 0. R by RING_3:def 5;
((Char R) '*' (1. R)) - (1. R) = ((Char R) '*' (1. R)) - (1 '*' (1. R)) by RING_3:60;
then F: ((Char R) - 1) '*' (1. R) = - (1. R) by C, RING_3:64;
reconsider n1 = (Char R) - 1 as Element of NAT by AS, INT_1:3;
deffunc H1( object ) -> Element of the carrier of R = 1. R;
consider f being FinSequence such that
D: ( len f = n1 & ( for k being Nat st k in dom f holds
f . k = H1(k) ) ) from FINSEQ_1:sch 2();
now :: thesis: for o being object st o in rng f holds
o in the carrier of R
let o be object ; :: thesis: ( o in rng f implies o in the carrier of R )
assume o in rng f ; :: thesis: o in the carrier of R
then consider k being object such that
E: ( k in dom f & o = f . k ) by FUNCT_1:def 3;
f . k = 1. R by E, D;
hence o in the carrier of R by E; :: thesis: verum
end;
then rng f c= the carrier of R ;
then reconsider f = f as FinSequence of R by FINSEQ_1:def 4;
now :: thesis: for k being Element of NAT st 1 <= k & k <= n1 holds
f /. k = 1. R
let k be Element of NAT ; :: thesis: ( 1 <= k & k <= n1 implies f /. k = 1. R )
assume ( 1 <= k & k <= n1 ) ; :: thesis: f /. k = 1. R
then E: k in dom f by D, FINSEQ_3:25;
hence f /. k = f . k by PARTFUN1:def 6
.= 1. R by E, D ;
:: thesis: verum
end;
then E: Sum f = n1 * (1. R) by D, POLYNOM8:4
.= - (1. R) by F, RING_3:def 2 ;
now :: thesis: for k being Nat st k in dom f holds
ex a being Element of R st f . k = a ^2
let k be Nat; :: thesis: ( k in dom f implies ex a being Element of R st f . k = a ^2 )
assume G: k in dom f ; :: thesis: ex a being Element of R st f . k = a ^2
1. R is square ;
hence ex a being Element of R st f . k = a ^2 by G, D; :: thesis: verum
end;
then - (1. R) is sum_of_squares by E;
then - (1. R) in QS R ;
then - (- (1. R)) in - the Preordering of R by B;
then 1. R in the Preordering of R /\ (- the Preordering of R) by A, XBOOLE_0:def 4;
then 1. R in {(0. R)} by defppc;
hence contradiction by TARSKI:def 1; :: thesis: verum
end;
hence Char R = 0 ; :: thesis: verum