let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: ex x being set st
( x in dom f & 0. = f . x ) ; :: thesis:
a2: for x being object st x in dom f holds
0. <= f . x by A2, SUPINF_2:39;
consider x0 being set such that
A4: x0 in dom f and
A5: 0. = f . x0 by A3;
reconsider x0 = x0 as Element of X by A4;
consider F1 being Finite_Sep_Sequence of S such that
A6: dom f = union (rng F1) and
A7: for n being Nat
for x, y being Element of X st n in dom F1 & x in F1 . n & y in F1 . n holds
f . x = f . y by A1, MESFUNC2:def 4;
consider V being set such that
A8: x0 in V and
A9: V in rng F1 by A4, A6, TARSKI:def 4;
consider n0 being object such that
A10: n0 in dom F1 and
A11: V = F1 . n0 by A9, FUNCT_1:def 3;
set F0 = { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } ;
set G1 = union { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } ;
for F9 being object st F9 in { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } holds
F9 in bool X

let F9 be object ; :: thesis:
assume F9 in { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } ; :: thesis:
then ex Fn being Element of S st
( F9 = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) ;
hence F9 in bool X ; :: thesis:

end;

then reconsider F0 = { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } as Subset-Family of X by TARSKI:def 3;
set N = { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } ;
A12: len F1 <= (len F1) + 1 by NAT_1:11;
reconsider n0 = n0 as Element of NAT by A10;
( F1 . n0 is Element of S & F1 . n0 in rng F1 & ( for x being Element of X st x in F1 . n0 holds
f . x = 0. ) )

F1 . n0 in rng F1 by A10, FUNCT_1:3;
hence F1 . n0 is Element of S ; :: thesis:
thus F1 . n0 in rng F1 by A10, FUNCT_1:3; :: thesis:
let x be Element of X; :: thesis:
assume x in F1 . n0 ; :: thesis:
hence f . x = 0. by A5, A7, A8, A10, A11; :: thesis:

end;

then A13: F1 . n0 in F0 ;
for z being object st z in F0 holds
z in rng F1

let z be object ; :: thesis:
assume z in F0 ; :: thesis:
then ex Fn9 being Element of S st
( z = Fn9 & Fn9 in rng F1 & ( for x being Element of X st x in Fn9 holds
f . x = 0. ) ) ;
hence z in rng F1 ; :: thesis:

end;

then A14: F0 c= rng F1 ;
for z being object st z in { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } holds
z in dom F1

let z be object ; :: thesis:
assume z in { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } ; :: thesis:
then ex n9 being Element of NAT st
( z = n9 & n9 in dom F1 & ( for x being Element of X st x in F1 . n9 holds
f . x = 0. ) ) ;
hence z in dom F1 ; :: thesis:

end;

then A15: { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } c= dom F1 ;
then reconsider N = { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds
f . x = 0. ) ) } as finite set ;
consider P1 being FinSequence such that
A16: ( rng P1 = N & P1 is one-to-one ) by FINSEQ_4:58;
reconsider F0 = F0 as N_Sub_set_fam of X by A14, A13;
for F9 being object st F9 in F0 holds
F9 in S

let F9 be object ; :: thesis:
assume F9 in F0 ; :: thesis:
then ex Fn being Element of S st
( F9 = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) ;
hence F9 in S ; :: thesis:

end;

then F0 c= S ;
then reconsider G1 = union { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) } as Element of S by MEASURE1:def 5;
A17: len P1 = card N by A16, FINSEQ_4:62;
reconsider L = Seg (len F1) as finite set ;
set M = (findom F1) \ N;
consider P2 being FinSequence such that
A18: rng P2 = (findom F1) \ N and
A19: P2 is one-to-one by FINSEQ_4:58;
A20: N c= Seg (len F1) by A15, FINSEQ_1:def 3;
then card N <= card L by NAT_1:43;
then len P1 <= len F1 by A17, FINSEQ_1:57;
then consider lenF being Nat such that
A21: (len F1) + 1 = (len P1) + lenF by A12, NAT_1:10, XXREAL_0:2;
reconsider lenF = lenF as Element of NAT by ORDINAL1:def 12;
(findom F1) \ N = (Seg (len F1)) \ N by FINSEQ_1:def 3;
then A22: card ((findom F1) \ N) = (card (Seg (len F1))) - (card N) by A20, CARD_2:44;
defpred S₁[ Nat, set ] means ( ( $1 = 1 implies $2 = G1 ) & ( $1 >= 2 implies ex k9 being Nat st
( k9 = $1 - 1 & $2 = F1 . (P2 . k9) ) ) );
len P2 = card ((findom F1) \ N) by A18, A19, FINSEQ_4:62;
then A23: len P2 = (((len F1) - (len P1)) + 1) - 1 by A17, A22, FINSEQ_1:57;
A24: for k being Nat st k in Seg lenF holds
ex U being Element of S st S₁[k,U]

let k be Nat; :: thesis:
assume A25: k in Seg lenF ; :: thesis:

suppose A26: k = 1 ; :: thesis:

take G1 ; :: thesis:
thus S₁[k,G1] by A26; :: thesis:

end;

suppose A27: k <> 1 ; :: thesis:

A28: k >= 1 by A25, FINSEQ_1:1;
then consider k9 being Nat such that
A29: k = 1 + k9 by NAT_1:10;
k > 1 by A27, A28, XXREAL_0:1;
then k >= 1 + 1 by NAT_1:13;
then A30: k - 1 >= 1 by XREAL_1:19;
k <= lenF by A25, FINSEQ_1:1;
then k - 1 <= lenF - 1 by XREAL_1:9;
then k9 in Seg (len P2) by A21, A23, A29, A30, FINSEQ_1:1;
then k9 in dom P2 by FINSEQ_1:def 3;
then P2 . k9 in (findom F1) \ N by A18, FUNCT_1:3;
then F1 . (P2 . k9) in rng F1 by FUNCT_1:3;
then reconsider U = F1 . (P2 . k9) as Element of S ;
take U ; :: thesis:
thus S₁[k,U] by A27, A29; :: thesis:

end;

end;

end;

consider F being FinSequence of S such that
A31: ( dom F = Seg lenF & ( for k being Nat st k in Seg lenF holds
S₁[k,F . k] ) ) from FINSEQ_1:sch 5(A24);
defpred S₂[ Nat, Element of ExtREAL ] means for y being Element of X holds
( ( y in F . $1 implies $2 = f . y ) & ( F . $1 = {} implies $2 = 1. ) );
A32: for k being Nat st k in Seg (len F) holds
ex x being Element of ExtREAL st S₂[k,x]

let k be Nat; :: thesis:
assume A33: k in Seg (len F) ; :: thesis:
then A34: k in dom F by FINSEQ_1:def 3;

case A35: k = 1 ; :: thesis:

take x = 0. ; :: thesis:
A36: F . k = G1 by A31, A34, A35;
for y being Element of X holds
( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) )

let y be Element of X; :: thesis:
( y in F . k implies 0. = f . y )

assume y in F . k ; :: thesis:
then consider Y being set such that
A37: y in Y and
A38: Y in F0 by A36, TARSKI:def 4;
ex Fn being Element of S st
( Y = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) by A38;
hence 0. = f . y by A37; :: thesis:

end;

hence ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) ) by A8, A11, A13, A36, TARSKI:def 4; :: thesis:

end;

hence ex x being Element of ExtREAL st S₂[k,x] ; :: thesis:

end;

case A39: k <> 1 ; :: thesis:

1 <= k by A33, FINSEQ_1:1;
then 1 < k by A39, XXREAL_0:1;
then A40: 1 + 1 <= k by NAT_1:13;
then consider k1 being Nat such that
A41: k1 = k - 1 and
A42: F . k = F1 . (P2 . k1) by A31, A34;
A43: 1 <= k1 by A40, A41, XREAL_1:19;
k <= lenF by A31, A34, FINSEQ_1:1;
then k1 <= len P2 by A21, A23, A41, XREAL_1:9;
then k1 in Seg (len P2) by A43, FINSEQ_1:1;
then k1 in dom P2 by FINSEQ_1:def 3;
then P2 . k1 in (findom F1) \ N by A18, FUNCT_1:3;
then consider k9 being set such that
A44: k9 in dom F1 and
A45: F . k = F1 . k9 by A42;

case A46: F . k = {} ; :: thesis:

take x = 1. ; :: thesis:
for y being Element of X holds
( ( y in F . k implies 1. = f . y ) & ( F . k = {} implies 1. = 1. ) ) by A46;
hence ex x being Element of ExtREAL st S₂[k,x] ; :: thesis:

end;

case F . k <> {} ; :: thesis:

then consider y1 being object such that
A47: y1 in F . k by XBOOLE_0:def 1;
F . k in rng F by A34, FUNCT_1:3;
then F . k in S ;
then reconsider y1 = y1 as Element of X by A47;
take x = f . y1; :: thesis:
for y being Element of X holds
( ( y in F . k implies x = f . y ) & ( F . k = {} implies x = 1. ) ) by A7, A44, A45, A47;
hence ex x being Element of ExtREAL st S₂[k,x] ; :: thesis:

end;

end;

end;

hence ex x being Element of ExtREAL st S₂[k,x] ; :: thesis:

end;

end;

end;

hence ex x being Element of ExtREAL st S₂[k,x] ; :: thesis:

end;

consider a being FinSequence of ExtREAL such that
A48: ( dom a = Seg (len F) & ( for n being Nat st n in Seg (len F) holds
S₂[n,a . n] ) ) from FINSEQ_1:sch 5(A32);
A49: for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume that
A50: n in dom F and
A51: x in F . n ; :: thesis:
n in Seg (len F) by A50, FINSEQ_1:def 3;
hence a . n = f . x by A48, A51; :: thesis:

end;

A52: for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n

let n be Nat; :: thesis:
assume A53: n in dom F ; :: thesis:
let x be object ; :: thesis:
assume A54: x in F . n ; :: thesis:
F . n in rng F by A53, FUNCT_1:3;
then F . n in S ;
then reconsider x = x as Element of X by A54;
a . n = f . x by A49, A53, A54;
hence f . x = a . n ; :: thesis:

end;

A55: for x being Element of X st x in F1 . n0 holds
f . x = 0. by A5, A7, A8, A10, A11;
A56: ( a . 1 = 0. & dom F = dom a & ( for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x ) )

reconsider F1n0 = F1 . n0 as Element of S by A9, A11;
0 + 1 <= lenF by A21, A23, XREAL_1:19;
then A57: 1 in Seg lenF by FINSEQ_1:1;
then A58: 1 in Seg (len F) by A31, FINSEQ_1:def 3;
A59: F . 1 = G1 by A31, A57;
F1n0 in F0 by A9, A11, A55;
then x0 in F . 1 by A8, A11, A59, TARSKI:def 4;
hence a . 1 = 0. by A5, A48, A58; :: thesis:
thus dom F = dom a by A48, FINSEQ_1:def 3; :: thesis:
thus for n being Nat
for x being Element of X st n in dom F & x in F . n holds
a . n = f . x by A49; :: thesis:

end;

A60: for n, m being Nat st n in dom F & m in dom F & n = 1 & m <> 1 holds
F . n misses F . m

let n, m be Nat; :: thesis:
assume that
A61: n in dom F and
A62: m in dom F and
A63: n = 1 and
A64: m <> 1 ; :: thesis:
A65: F . n = G1 by A31, A61, A63;
m <= lenF by A31, A62, FINSEQ_1:1;
then A66: m - 1 <= lenF - 1 by XREAL_1:9;
1 <= m by A62, FINSEQ_3:25;
then 1 < m by A64, XXREAL_0:1;
then A67: 1 + 1 <= m by NAT_1:13;
then consider k9 being Nat such that
A68: k9 = m - 1 and
A69: F . m = F1 . (P2 . k9) by A31, A62;
m - 1 >= 1 by A67, XREAL_1:19;
then k9 in Seg (len P2) by A21, A23, A68, A66, FINSEQ_1:1;
then k9 in dom P2 by FINSEQ_1:def 3;
then A70: P2 . k9 in (findom F1) \ N by A18, FUNCT_1:3;
then A71: not P2 . k9 in N by XBOOLE_0:def 5;
(F . n) /\ (F . m) = {}

assume (F . n) /\ (F . m) <> {} ; :: thesis:
then consider v being object such that
A72: v in (F . n) /\ (F . m) by XBOOLE_0:def 1;
A73: v in F . m by A72, XBOOLE_0:def 4;
v in F . n by A72, XBOOLE_0:def 4;
then consider Y being set such that
A74: v in Y and
A75: Y in F0 by A65, TARSKI:def 4;
consider Fv being Element of S such that
A76: Y = Fv and
A77: Fv in rng F1 and
A78: for x being Element of X st x in Fv holds
f . x = 0. by A75;
consider n9 being object such that
A79: n9 in dom F1 and
A80: Fv = F1 . n9 by A77, FUNCT_1:def 3;
reconsider n9 = n9 as Element of NAT by A79;
n9 <> P2 . k9 by A70, A71, A78, A80;
then F1 . n9 misses F1 . (P2 . k9) by PROB_2:def 2;
then (F1 . n9) /\ (F1 . (P2 . k9)) = {} ;
hence contradiction by A69, A73, A74, A76, A80, XBOOLE_0:def 4; :: thesis:

end;

hence F . n misses F . m ; :: thesis:

end;

A81: for n, m being Nat st n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m holds
F . n misses F . m

let n, m be Nat; :: thesis:
assume that
A82: n in dom F and
A83: m in dom F and
A84: n <> 1 and
A85: m <> 1 and
A86: n <> m ; :: thesis:
n <= lenF by A31, A82, FINSEQ_1:1;
then A87: n - 1 <= lenF - 1 by XREAL_1:9;
m <= lenF by A31, A83, FINSEQ_1:1;
then A88: m - 1 <= lenF - 1 by XREAL_1:9;
1 <= m by A31, A83, FINSEQ_1:1;
then 1 < m by A85, XXREAL_0:1;
then A89: 1 + 1 <= m by NAT_1:13;
then consider k2 being Nat such that
A90: k2 = m - 1 and
A91: F . m = F1 . (P2 . k2) by A31, A83;
1 <= m - 1 by A89, XREAL_1:19;
then k2 in Seg (len P2) by A21, A23, A90, A88, FINSEQ_1:1;
then A92: k2 in dom P2 by FINSEQ_1:def 3;
1 <= n by A31, A82, FINSEQ_1:1;
then 1 < n by A84, XXREAL_0:1;
then A93: 1 + 1 <= n by NAT_1:13;
then consider k1 being Nat such that
A94: k1 = n - 1 and
A95: F . n = F1 . (P2 . k1) by A31, A82;
1 <= n - 1 by A93, XREAL_1:19;
then k1 in Seg (len P2) by A21, A23, A94, A87, FINSEQ_1:1;
then A96: k1 in dom P2 by FINSEQ_1:def 3;
k1 <> k2 by A86, A94, A90;
then P2 . k1 <> P2 . k2 by A19, A96, A92, FUNCT_1:def 4;
hence F . n misses F . m by A95, A91, PROB_2:def 2; :: thesis:

end;

A97: for x, y being object st x <> y holds
F . x misses F . y

let x, y be object ; :: thesis:
assume A98: x <> y ; :: thesis:

case A99: ( x in dom F & y in dom F ) ; :: thesis:

then reconsider x = x, y = y as Element of NAT ;

case ( x = 1 or y = 1 ) ; :: thesis:

hence F . x misses F . y by A60, A98, A99; :: thesis:

end;

case ( x <> 1 & y <> 1 ) ; :: thesis:

hence F . x misses F . y by A81, A98, A99; :: thesis:

end;

end;

end;

hence F . x misses F . y ; :: thesis:

end;

case A100: ( not x in dom F or not y in dom F ) ; :: thesis:

per cases by A100;

case not x in dom F ; :: thesis:

then F . x = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis:

end;

case not y in dom F ; :: thesis:

then F . y = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis:

end;

end;

end;

hence F . x misses F . y ; :: thesis:

end;

end;

end;

hence F . x misses F . y ; :: thesis:

end;

for z being object st z in union (rng F) holds
z in union (rng F1)

let z be object ; :: thesis:
assume z in union (rng F) ; :: thesis:
then consider Y being set such that
A101: z in Y and
A102: Y in rng F by TARSKI:def 4;
consider k being object such that
A103: k in dom F and
A104: Y = F . k by A102, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A103;

case k = 1 ; :: thesis:

then z in G1 by A31, A101, A103, A104;
then consider Y9 being set such that
A105: z in Y9 and
A106: Y9 in F0 by TARSKI:def 4;
ex Fn9 being Element of S st
( Y9 = Fn9 & Fn9 in rng F1 & ( for x being Element of X st x in Fn9 holds
f . x = 0. ) ) by A106;
hence z in union (rng F1) by A105, TARSKI:def 4; :: thesis:

end;

case A107: k <> 1 ; :: thesis:

1 <= k by A31, A103, FINSEQ_1:1;
then 1 < k by A107, XXREAL_0:1;
then A108: 1 + 1 <= k by NAT_1:13;
then consider k9 being Nat such that
A109: k9 = k - 1 and
A110: F . k = F1 . (P2 . k9) by A31, A103;
A111: 1 <= k9 by A108, A109, XREAL_1:19;
k <= lenF by A31, A103, FINSEQ_1:1;
then k9 <= len P2 by A21, A23, A109, XREAL_1:9;
then k9 in dom P2 by A111, FINSEQ_3:25;
then P2 . k9 in (findom F1) \ N by A18, FUNCT_1:3;
then F1 . (P2 . k9) in rng F1 by FUNCT_1:3;
hence z in union (rng F1) by A101, A104, A110, TARSKI:def 4; :: thesis:

end;

end;

end;

hence z in union (rng F1) ; :: thesis:

end;

then A112: union (rng F) c= union (rng F1) ;
for z being object st z in union (rng F1) holds
z in union (rng F)

let z be object ; :: thesis:
assume z in union (rng F1) ; :: thesis:
then consider Y being set such that
A113: z in Y and
A114: Y in rng F1 by TARSKI:def 4;
consider m1 being object such that
A115: m1 in dom F1 and
A116: Y = F1 . m1 by A114, FUNCT_1:def 3;
reconsider m1 = m1 as Element of NAT by A115;

case m1 in N ; :: thesis:

then ex m19 being Element of NAT st
( m1 = m19 & m19 in dom F1 & ( for x being Element of X st x in F1 . m19 holds
f . x = 0. ) ) ;
then Y in F0 by A114, A116;
then A117: z in union F0 by A113, TARSKI:def 4;
lenF >= 1 + 0 by A21, A23, XREAL_1:19;
then A118: 1 in Seg lenF by FINSEQ_1:1;
then F . 1 in rng F by A31, FUNCT_1:3;
then union F0 in rng F by A31, A118;
hence z in union (rng F) by A117, TARSKI:def 4; :: thesis:

end;

case not m1 in N ; :: thesis:

then m1 in (findom F1) \ N by A115, XBOOLE_0:def 5;
then consider m19 being object such that
A119: m19 in dom P2 and
A120: m1 = P2 . m19 by A18, FUNCT_1:def 3;
reconsider m19 = m19 as Element of NAT by A119;
A121: m19 in Seg (len P2) by A119, FINSEQ_1:def 3;
then m19 <= len P2 by FINSEQ_1:1;
then A122: m19 + 1 <= lenF by A21, A23, XREAL_1:6;
reconsider m2 = m19 + 1 as Nat ;
1 <= m19 by A121, FINSEQ_1:1;
then A123: 1 + 1 <= m19 + 1 by XREAL_1:6;
then 1 <= m2 by XXREAL_0:2;
then A124: m2 in Seg lenF by A122, FINSEQ_1:1;
then A125: F . m2 in rng F by A31, FUNCT_1:3;
ex k9 being Nat st
( k9 = m2 - 1 & F . m2 = F1 . (P2 . k9) ) by A31, A123, A124;
hence z in union (rng F) by A113, A116, A120, A125, TARSKI:def 4; :: thesis:

end;

end;

end;

hence z in union (rng F) ; :: thesis:

end;

then union (rng F1) c= union (rng F) ;
then A126: union (rng F) = dom f by A6, A112;
reconsider F = F as Finite_Sep_Sequence of S by A97, PROB_2:def 2;
take F ; :: thesis:
take a ; :: thesis:
for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty )

A127: f is real-valued by A1, MESFUNC2:def 4;
0 + 1 <= lenF by A21, A23, XREAL_1:19;
then A128: 1 in dom F by A31, FINSEQ_1:1;
let n be Nat; :: thesis:
assume that
A129: 2 <= n and
A130: n in dom a ; :: thesis:
1 + 1 <= n by A129;
then A131: 1 <= n - 1 by XREAL_1:19;
consider k1 being Nat such that
A132: k1 = n - 1 and
A133: F . n = F1 . (P2 . k1) by A31, A56, A129, A130;
n <= lenF by A31, A56, A130, FINSEQ_1:1;
then n - 1 <= lenF - 1 by XREAL_1:9;
then k1 in Seg (len P2) by A21, A23, A132, A131, FINSEQ_1:1;
then k1 in dom P2 by FINSEQ_1:def 3;
then P2 . k1 in (findom F1) \ N by A18, FUNCT_1:3;
then A134: F . n in rng F1 by A133, FUNCT_1:3;
n <> 1 by A129;
then F . 1 misses F . n by A56, A60, A130, A128;
then A135: G1 misses F . n by A31, A128;
( a . n <> 0. & 0. <= a . n & a . n < +infty )

suppose A136: F . n <> {} ; :: thesis:

A137: F . n in rng F by A56, A130, FUNCT_1:3;
then reconsider Fn = F . n as Element of S ;
consider y being object such that
A138: y in F . n by A136, XBOOLE_0:def 1;
F . n in S by A137;
then reconsider y = y as Element of X by A138;
A139: a . n = f . y by A48, A130, A138;
G1 /\ (F . n) = {} by A135;
then A140: not y in G1 by A138, XBOOLE_0:def 4;
thus a . n <> 0. :: thesis:

assume a . n = 0. ; :: thesis:
then for x being Element of X st x in F . n holds
f . x = 0. by A56, A130;
then Fn in F0 by A134;
hence contradiction by A138, A140, TARSKI:def 4; :: thesis:

end;

A141: y in union (rng F) by A138, A137, TARSKI:def 4;
then |.(f . y).| < +infty by A6, A112, A127, MESFUNC2:def 1;
hence ( 0. <= a . n & a . n < +infty ) by A6, A112, A139, A141, EXTREAL1:21, a2; :: thesis:

end;

suppose A142: F . n = {} ; :: thesis:

hence a . n <> 0. by A48, A130; :: thesis:
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
thus 0. <= a . n by A48, A130, A142; :: thesis:
S₂[n,a . n] by A48, A130;
then a . n = jj by A142;
hence a . n < +infty by XXREAL_0:9; :: thesis:

end;

end;

end;

hence ( 0. < a . n & a . n < +infty ) ; :: thesis:

end;

hence ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) ) by A126, A56, A52; :: thesis: