let K be Field; :: thesis: for f being Field-yielding ascending sequence st ( for i being Element of NAT holds f . i is Subfield of K ) holds
SeqField f is Subfield of K
let f be Field-yielding ascending sequence ; :: thesis: ( ( for i being Element of NAT holds f . i is Subfield of K ) implies SeqField f is Subfield of K )
assume AS: for i being Element of NAT holds f . i is Subfield of K ; :: thesis: SeqField f is Subfield of K
then X: f . 0 is Subfield of K ;
set F = 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 } ;
A: the carrier of (SeqField f) c= the carrier of K

proof

now :: thesis: for o being object st o in the carrier of (SeqField f) holds
o in the carrier of K

let o be object ; :: thesis: ( o in the carrier of (SeqField f) implies o in the carrier of K )
assume o in the carrier of (SeqField f) ; :: thesis: o in the carrier of K
then consider Y being set such that
A1: ( o in Y & Y in { the carrier of (f . i) where i is Element of NAT : verum } ) by H, TARSKI:def 4;
consider i being Element of NAT such that
A2: Y = the carrier of (f . i) by A1;
f . i is Subfield of K by AS;
then the carrier of (f . i) c= the carrier of K by EC_PF_1:def 1;
hence o in the carrier of K by A1, A2; :: thesis: verum

end;

hence the carrier of (SeqField f) c= the carrier of K ; :: thesis: verum

end;

B: the addF of (SeqField f) = the addF of K || the carrier of (SeqField f)

proof

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

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

let x be object ; :: thesis: ( x in dom the addF of (SeqField f) implies the addF of (SeqField f) . b₁ = ( the addF of K || the carrier of (SeqField f)) . b₁ )
assume x in dom the addF of (SeqField f) ; :: thesis: the addF of (SeqField f) . b₁ = ( the addF of K || the carrier of (SeqField f)) . b₁
then consider a, b being object such that
B3: ( a in the carrier of (SeqField f) & b in the carrier of (SeqField f) & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of (SeqField f) by B3;
consider Y1 being set such that
C1: ( a in Y1 & Y1 in { the carrier of (f . i) where i is Element of NAT : verum } ) by H, TARSKI:def 4;
consider j1 being Element of NAT such that
B4: Y1 = the carrier of (f . j1) by C1;
consider Y2 being set such that
C2: ( b in Y2 & Y2 in { the carrier of (f . i) where i is Element of NAT : verum } ) by H, TARSKI:def 4;
consider j2 being Element of NAT such that
B5: Y2 = the carrier of (f . j2) by C2;

per cases ( j1 <= j2 or j2 <= j1 ) ;

suppose j1 <= j2 ; :: thesis: the addF of (SeqField f) . b₁ = ( the addF of K || the carrier of (SeqField f)) . b₁

then reconsider a1 = a, b1 = b as Element of (f . j2) by C1, C2, B4, B5, lem1;
f . j2 is Subfield of K by AS;
then B4: the addF of (f . j2) = the addF of K || the carrier of (f . j2) by EC_PF_1:def 1;
B5: [a1,b1] in [: the carrier of (f . j2), the carrier of (f . j2):] by ZFMISC_1:def 2;
B6: [a1,b1] in [: the carrier of (SeqField f), the carrier of (SeqField f):] by ZFMISC_1:def 2;
thus the addF of (SeqField f) . x = a + b by B3
.= a1 + b1 by lem4
.= the addF of K . (a1,b1) by B4, B5, FUNCT_1:49
.= ( the addF of K || the carrier of (SeqField f)) . x by B3, B6, FUNCT_1:49 ; :: thesis: verum

end;

suppose j2 <= j1 ; :: thesis: the addF of (SeqField f) . b₁ = ( the addF of K || the carrier of (SeqField f)) . b₁

then reconsider a1 = a, b1 = b as Element of (f . j1) by C1, C2, B4, B5, lem1;
f . j1 is Subfield of K by AS;
then B4: the addF of (f . j1) = the addF of K || the carrier of (f . j1) by EC_PF_1:def 1;
B5: [a1,b1] in [: the carrier of (f . j1), the carrier of (f . j1):] by ZFMISC_1:def 2;
B6: [a1,b1] in [: the carrier of (SeqField f), the carrier of (SeqField f):] by ZFMISC_1:def 2;
thus the addF of (SeqField f) . x = a + b by B3
.= a1 + b1 by lem4
.= the addF of K . (a1,b1) by B4, B5, FUNCT_1:49
.= ( the addF of K || the carrier of (SeqField f)) . x by B3, B6, FUNCT_1:49 ; :: thesis: verum

end;

end;

end;

hence the addF of (SeqField f) = the addF of K || the carrier of (SeqField f) by B1; :: thesis: verum

end;

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

proof

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

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

let x be object ; :: thesis: ( x in dom the multF of (SeqField f) implies the multF of (SeqField f) . b₁ = ( the multF of K || the carrier of (SeqField f)) . b₁ )
assume x in dom the multF of (SeqField f) ; :: thesis: the multF of (SeqField f) . b₁ = ( the multF of K || the carrier of (SeqField f)) . b₁
then consider a, b being object such that
B3: ( a in the carrier of (SeqField f) & b in the carrier of (SeqField f) & x = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Element of (SeqField f) by B3;
consider Y1 being set such that
C1: ( a in Y1 & Y1 in { the carrier of (f . i) where i is Element of NAT : verum } ) by H, TARSKI:def 4;
consider j1 being Element of NAT such that
B4: Y1 = the carrier of (f . j1) by C1;
consider Y2 being set such that
C2: ( b in Y2 & Y2 in { the carrier of (f . i) where i is Element of NAT : verum } ) by H, TARSKI:def 4;
consider j2 being Element of NAT such that
B5: Y2 = the carrier of (f . j2) by C2;

per cases ( j1 <= j2 or j2 <= j1 ) ;

suppose j1 <= j2 ; :: thesis: the multF of (SeqField f) . b₁ = ( the multF of K || the carrier of (SeqField f)) . b₁

then reconsider a1 = a, b1 = b as Element of (f . j2) by C1, C2, B4, B5, lem1;
f . j2 is Subfield of K by AS;
then B4: the multF of (f . j2) = the multF of K || the carrier of (f . j2) by EC_PF_1:def 1;
B5: [a1,b1] in [: the carrier of (f . j2), the carrier of (f . j2):] by ZFMISC_1:def 2;
B6: [a1,b1] in [: the carrier of (SeqField f), the carrier of (SeqField f):] by ZFMISC_1:def 2;
thus the multF of (SeqField f) . x = a * b by B3
.= a1 * b1 by lem4
.= the multF of K . (a1,b1) by B4, B5, FUNCT_1:49
.= ( the multF of K || the carrier of (SeqField f)) . x by B3, B6, FUNCT_1:49 ; :: thesis: verum

end;

suppose j2 <= j1 ; :: thesis: the multF of (SeqField f) . b₁ = ( the multF of K || the carrier of (SeqField f)) . b₁

then reconsider a1 = a, b1 = b as Element of (f . j1) by C1, C2, B4, B5, lem1;
f . j1 is Subfield of K by AS;
then B4: the multF of (f . j1) = the multF of K || the carrier of (f . j1) by EC_PF_1:def 1;
B5: [a1,b1] in [: the carrier of (f . j1), the carrier of (f . j1):] by ZFMISC_1:def 2;
B6: [a1,b1] in [: the carrier of (SeqField f), the carrier of (SeqField f):] by ZFMISC_1:def 2;
thus the multF of (SeqField f) . x = a * b by B3
.= a1 * b1 by lem4
.= the multF of K . (a1,b1) by B4, B5, FUNCT_1:49
.= ( the multF of K || the carrier of (SeqField f)) . x by B3, B6, FUNCT_1:49 ; :: thesis: verum

end;

end;

end;

hence the multF of (SeqField f) = the multF of K || the carrier of (SeqField f) by B1; :: thesis: verum

end;

D: 1. (SeqField f) = 1. (f . 0) by dsf
.= 1. K by X, EC_PF_1:def 1 ;
0. (SeqField f) = 0. (f . 0) by dsf
.= 0. K by X, EC_PF_1:def 1 ;
hence SeqField f is Subfield of K by A, B, C, D, EC_PF_1:def 1; :: thesis: verum