let f be Field-yielding ascending sequence ; :: thesis: for i, j being Element of NAT
for xi, yi being Element of (f . i)
for xj, yj being Element of (f . j) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
let i, j be Element of NAT ; :: thesis: for xi, yi being Element of (f . i)
for xj, yj being Element of (f . j) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
let xi, yi be Element of (f . i); :: thesis: for xj, yj being Element of (f . j) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
let xj, yj be Element of (f . j); :: thesis: ( xi = xj & yi = yj implies ( xi + yi = xj + yj & xi * yi = xj * yj ) )
assume AS2: ( xi = xj & yi = yj ) ; :: thesis: ( xi + yi = xj + yj & xi * yi = xj * yj )

per cases ( i <= j or j <= i ) ;

suppose AS1: i <= j ; :: thesis: ( xi + yi = xj + yj & xi * yi = xj * yj )

defpred S₁[ Nat] means ex k being Element of NAT st
( k = i + $1 & ( for xi, yi being Element of (f . i)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ) );
IA: S₁[ 0 ]

proof

take k = i; :: thesis: ( k = i + 0 & ( for xi, yi being Element of (f . i)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ) )
thus k = i + 0 ; :: thesis: for xi, yi being Element of (f . i)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
thus for xi, yi being Element of (f . i)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider n being Element of NAT such that
IV: ( n = i + k & ( for xi, yi being Element of (f . i)
for xj, yj being Element of (f . n) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ) ) ;

now :: thesis: for xi, yi being Element of (f . i)
for xj, yj being Element of (f . (n + 1)) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )

let xi, yi be Element of (f . i); :: thesis: for xj, yj being Element of (f . (n + 1)) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
let xj, yj be Element of (f . (n + 1)); :: thesis: ( xi = xj & yi = yj implies ( xi + yi = xj + yj & xi * yi = xj * yj ) )
assume B: ( xi = xj & yi = yj ) ; :: thesis: ( xi + yi = xj + yj & xi * yi = xj * yj )
( i <= i + k & i + k <= n + 1 ) by IV, NAT_1:11;
then f . (n + 1) is FieldExtension of f . i by lem3, XXREAL_0:2;
then f . i is Subfield of f . (n + 1) by FIELD_4:7;
then C: f . i is Subring of f . (n + 1) by FIELD_5:12;
hence xi + yi = xj + yj by B, FIELD_6:15; :: thesis: xi * yi = xj * yj
thus xi * yi = xj * yj by B, C, FIELD_6:16; :: thesis: verum

end;

hence S₁[k + 1] by IV; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: i + n = j by AS1, NAT_1:10;
S₁[n] by I;
hence ( xi + yi = xj + yj & xi * yi = xj * yj ) by H, AS2; :: thesis: verum

end;

suppose AS1: j <= i ; :: thesis: ( xi + yi = xj + yj & xi * yi = xj * yj )

defpred S₁[ Nat] means ex k being Element of NAT st
( k = j + $1 & ( for xi, yi being Element of (f . j)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ) );
IA: S₁[ 0 ]

proof

take k = j; :: thesis: ( k = j + 0 & ( for xi, yi being Element of (f . j)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ) )
thus k = j + 0 ; :: thesis: for xi, yi being Element of (f . j)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
thus for xi, yi being Element of (f . j)
for xj, yj being Element of (f . k) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ; :: thesis: verum

end;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider n being Element of NAT such that
IV: ( n = j + k & ( for xi, yi being Element of (f . j)
for xj, yj being Element of (f . n) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj ) ) ) ;

now :: thesis: for xi, yi being Element of (f . j)
for xj, yj being Element of (f . (n + 1)) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )

let xi, yi be Element of (f . j); :: thesis: for xj, yj being Element of (f . (n + 1)) st xi = xj & yi = yj holds
( xi + yi = xj + yj & xi * yi = xj * yj )
let xj, yj be Element of (f . (n + 1)); :: thesis: ( xi = xj & yi = yj implies ( xi + yi = xj + yj & xi * yi = xj * yj ) )
assume B: ( xi = xj & yi = yj ) ; :: thesis: ( xi + yi = xj + yj & xi * yi = xj * yj )
( j <= j + k & j + k <= n + 1 ) by IV, NAT_1:11;
then f . (n + 1) is FieldExtension of f . j by lem3, XXREAL_0:2;
then f . j is Subfield of f . (n + 1) by FIELD_4:7;
then C: f . j is Subring of f . (n + 1) by FIELD_5:12;
hence xi + yi = xj + yj by B, FIELD_6:15; :: thesis: xi * yi = xj * yj
thus xi * yi = xj * yj by B, C, FIELD_6:16; :: thesis: verum

end;

hence S₁[k + 1] by IV; :: thesis: verum

end;

I: for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
consider n being Nat such that
H: j + n = i by AS1, NAT_1:10;
S₁[n] by I;
hence ( xi + yi = xj + yj & xi * yi = xj * yj ) by H, AS2; :: thesis: verum

end;

end;