let f be Field-yielding ascending sequence ; :: thesis: for i being Element of NAT holds f . i is Subfield of SeqField f
let i be Element of NAT ; :: thesis: f . i is Subfield of SeqField f
set F = f . i;
set K = SeqField f;
H: the carrier of (SeqField f) = Carrier f by dsf
.= union { the carrier of (f . i) where i is Element of NAT : verum } ;
J: the carrier of (f . i) in { the carrier of (f . i) where i is Element of NAT : verum } ;
then A: the carrier of (f . i) c= the carrier of (SeqField f) by H, ZFMISC_1:74;
B: the addF of (f . i) = the addF of (SeqField f) || the carrier of (f . i)

proof

set aF = the addF of (f . i);
set aK = the addF of (SeqField f) || the carrier of (f . i);
B1: dom ( the addF of (SeqField f) || the carrier of (f . i)) = (dom the addF of (SeqField f)) /\ [: the carrier of (f . i), the carrier of (f . i):] by RELAT_1:61
.= [: the carrier of (SeqField f), the carrier of (SeqField f):] /\ [: the carrier of (f . i), the carrier of (f . i):] by FUNCT_2:def 1
.= [: the carrier of (f . i), the carrier of (f . i):] by A, ZFMISC_1:96, XBOOLE_1:28 ;

now :: thesis: for x being object st x in dom the addF of (f . i) holds
the addF of (f . i) . x = ( the addF of (SeqField f) || the carrier of (f . i)) . x

let x be object ; :: thesis: ( x in dom the addF of (f . i) implies the addF of (f . i) . x = ( the addF of (SeqField f) || the carrier of (f . i)) . x )
assume B2: x in dom the addF of (f . i) ; :: thesis: the addF of (f . i) . x = ( the addF of (SeqField f) || the carrier of (f . i)) . x
then consider a, b being object such that
B3: ( a in the carrier of (f . i) & b in the carrier of (f . i) & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of (f . i) by B3;
reconsider y = a, z = b as Element of (SeqField f) by A;
thus the addF of (f . i) . x = a + b by B3
.= y + z by lem4
.= ( the addF of (SeqField f) || the carrier of (f . i)) . x by B3, B2, FUNCT_1:49 ; :: thesis: verum

end;

hence the addF of (f . i) = the addF of (SeqField f) || the carrier of (f . i) by B1, FUNCT_2:def 1; :: thesis: verum

end;

C: the multF of (f . i) = the multF of (SeqField f) || the carrier of (f . i)

proof

set mF = the multF of (f . i);
set mK = the multF of (SeqField f) || the carrier of (f . i);
B1: dom ( the multF of (SeqField f) || the carrier of (f . i)) = (dom the multF of (SeqField f)) /\ [: the carrier of (f . i), the carrier of (f . i):] by RELAT_1:61
.= [: the carrier of (SeqField f), the carrier of (SeqField f):] /\ [: the carrier of (f . i), the carrier of (f . i):] by FUNCT_2:def 1
.= [: the carrier of (f . i), the carrier of (f . i):] by A, ZFMISC_1:96, XBOOLE_1:28 ;

now :: thesis: for x being object st x in dom the multF of (f . i) holds
the multF of (f . i) . x = ( the multF of (SeqField f) || the carrier of (f . i)) . x

let x be object ; :: thesis: ( x in dom the multF of (f . i) implies the multF of (f . i) . x = ( the multF of (SeqField f) || the carrier of (f . i)) . x )
assume B2: x in dom the multF of (f . i) ; :: thesis: the multF of (f . i) . x = ( the multF of (SeqField f) || the carrier of (f . i)) . x
then consider a, b being object such that
B3: ( a in the carrier of (f . i) & b in the carrier of (f . i) & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of (f . i) by B3;
reconsider y = a, z = b as Element of (SeqField f) by A;
thus the multF of (f . i) . x = a * b by B3
.= y * z by lem4
.= ( the multF of (SeqField f) || the carrier of (f . i)) . x by B3, B2, FUNCT_1:49 ; :: thesis: verum

end;

hence the multF of (f . i) = the multF of (SeqField f) || the carrier of (f . i) by B1, FUNCT_2:def 1; :: thesis: verum

end;

( 1. (f . i) = 1. (SeqField f) & 0. (f . i) = 0. (SeqField f) ) by lem5;
hence f . i is Subfield of SeqField f by H, J, ZFMISC_1:74, B, C, EC_PF_1:def 1; :: thesis: verum