defpred S₁[ object , Field, Field] means ( $3 is FieldExtension of $2 & ( for K being FieldExtension of $2 st K = $3 holds
for p being non constant Element of the carrier of (Polynom-Ring $2) holds p is_with_roots_in K ) );
A: for n being Nat
for x being Field ex y being Field st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Field ex y being Field st S₁[n,x,y]
let x be Field; :: thesis: ex y being Field st S₁[n,x,y]
consider y being FieldExtension of x such that
A1: for p being non constant Element of the carrier of (Polynom-Ring x) holds p is_with_roots_in y by FIELD_11:43;
take y ; :: thesis: S₁[n,x,y]
thus S₁[n,x,y] by A1; :: thesis: verum

end;

consider f being Field-yielding sequence such that
B: ( f . 0 = F & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from FIELD_12:sch 1(A);
for i being Element of NAT holds f . (i + 1) is FieldExtension of f . i by B;
then reconsider f = f as Field-yielding ascending sequence by defasc;
take f ; :: thesis: ( f . 0 = F & ( for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = f . i & E = f . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E ) )
thus f . 0 = F by B; :: thesis: for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = f . i & E = f . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E
thus for i being Element of NAT
for K being Field
for E being FieldExtension of K st K = f . i & E = f . (i + 1) holds
for p being non constant Element of the carrier of (Polynom-Ring K) holds p is_with_roots_in E by B; :: thesis: verum