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: for x being set st x in dom f holds
0. <= f . x and
A3: ex x being set st
( x in dom f & 0. = f . x ) ; :: thesis:
consider x0 being set such that
A4: ( x0 in dom f & 0. = f . x0 ) by A3;
reconsider x0 = x0 as Element of X by A4;
consider F1 being Finite_Sep_Sequence of S such that
A5: ( dom f = union (rng F1) & ( 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 5;
consider V being set such that
A6: ( x0 in V & V in rng F1 ) by A4, A5, TARSKI:def 4;
consider n0 being set such that
A7: ( n0 in dom F1 & V = F1 . n0 ) by A6, FUNCT_1:def 5;
reconsider n0 = n0 as Element of NAT by A7;
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. ) ) } ;
A8: for x being Element of X st x in F1 . n0 holds
f . x = 0. by A4, A5, A6, A7;
for z being set 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 set ; :: 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 consider n' being Element of NAT such that
A9: ( z = n' & n' in dom F1 & ( for x being Element of X st x in F1 . n' holds
f . x = 0. ) ) ;
thus z in dom F1 by A9; :: thesis:

end;

then A10: { 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 by TARSKI:def 3;
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
A11: ( rng P1 = N & P1 is one-to-one ) by FINSEQ_4:73;
set M = (findom F1) \ N;
consider P2 being FinSequence such that
A12: ( rng P2 = (findom F1) \ N & P2 is one-to-one ) by FINSEQ_4:73;
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 F' being set st F' 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
F' in bool X

let F' be set ; :: thesis:
assume F' 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 consider Fn being Element of S such that
A13: ( F' = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) ;
thus F' in bool X by A13; :: 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;
defpred S₁[ set , set ] means ( ( $1 in dom F1 implies $2 = F1 . $1 ) & ( not $1 in dom F1 implies $2 = {} ) );
consider F2 being Function of NAT ,S;
for z being set st z in F0 holds
z in rng F1

let z be set ; :: thesis:
assume z in F0 ; :: thesis:
then consider Fn' being Element of S such that
A22: ( z = Fn' & Fn' in rng F1 & ( for x being Element of X st x in Fn' holds
f . x = 0. ) ) ;
thus z in rng F1 by A22; :: thesis:

end;

then A23: F0 c= rng F1 by TARSKI:def 3;
( 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. ) )

consider n0' being Nat such that
A24: ( n0 = n0' & n0' in dom F1 & ( for x being Element of X st x in F1 . n0' holds
f . x = 0. ) ) by A7, A8;
( F1 . n0 in rng F1 & rng F1 c= S ) by A24, FUNCT_1:12;
hence F1 . n0 is Element of S ; :: thesis:
thus F1 . n0 in rng F1 by A24, FUNCT_1:12; :: thesis:
let x be Element of X; :: thesis:
assume x in F1 . n0 ; :: thesis:
hence f . x = 0. by A24; :: thesis:

end;

then A25: F1 . n0 in F0 ;
then reconsider F0 = F0 as N_Sub_set_fam of X by A23;
for F' being set st F' in F0 holds
F' in S

let F' be set ; :: thesis:
assume F' in F0 ; :: thesis:
then consider Fn being Element of S such that
A26: ( F' = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) ;
thus F' in S by A26; :: thesis:

end;

then F0 c= S by TARSKI:def 3;
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 9;
A27: ( len P1 = card N & len P2 = card ((findom F1) \ N) ) by A11, A12, FINSEQ_4:77;
reconsider L = Seg (len F1) as finite set ;
A28: N c= Seg (len F1) by A10, FINSEQ_1:def 3;
then card N <= card L by NAT_1:44;
then ( len P1 <= len F1 & len F1 <= (len F1) + 1 ) by A27, FINSEQ_1:78, NAT_1:11;
then consider lenF being Nat such that
A29: (len F1) + 1 = (len P1) + lenF by NAT_1:10, XXREAL_0:2;
reconsider lenF = lenF as Element of NAT by ORDINAL1:def 13;
(findom F1) \ N = (Seg (len F1)) \ N by FINSEQ_1:def 3;
then card ((findom F1) \ N) = (card (Seg (len F1))) - (card N) by A28, CARD_2:63;
then A30: len P2 = (((len F1) - (len P1)) + 1) - 1 by A27, FINSEQ_1:78;
defpred S₂[ Nat, set ] means ( ( $1 = 1 implies $2 = G1 ) & ( $1 >= 2 implies ex k' being Nat st
( k' = $1 - 1 & $2 = F1 . (P2 . k') ) ) );
A31: 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 A32: k in Seg lenF ; :: thesis:

per cases ;

suppose A33: k = 1 ; :: thesis:

take U = G1; :: thesis:
thus S₂[k,U] by A33; :: thesis:

end;

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

A35: ( k >= 1 & k <= lenF ) by A32, FINSEQ_1:3;
then k > 1 by A34, XXREAL_0:1;
then A36: k >= 1 + 1 by NAT_1:13;
consider k' being Nat such that
A37: k = 1 + k' by A35, NAT_1:10;
( k - 1 >= 1 & k - 1 <= lenF - 1 ) by A35, A36, XREAL_1:11, XREAL_1:21;
then k' in Seg (len P2) by A29, A30, A37, FINSEQ_1:3;
then k' in dom P2 by FINSEQ_1:def 3;
then P2 . k' in (findom F1) \ N by A12, FUNCT_1:12;
then ( F1 . (P2 . k') in rng F1 & rng F1 c= S ) by FUNCT_1:12;
then reconsider U = F1 . (P2 . k') as Element of S ;
take U ; :: thesis:
thus S₂[k,U] by A34, A37; :: thesis:

end;

end;

end;

consider F being FinSequence of S such that
A38: ( dom F = Seg lenF & ( for k being Nat st k in Seg lenF holds
S₂[k,F . k] ) ) from FINSEQ_1:sch 5(A31);
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. ) );
A39: 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 k in Seg (len F) ; :: thesis:
then A40: k in dom F by FINSEQ_1:def 3;

now

per cases ;

case k = 1 ; :: thesis:

then A41: F . k = G1 by A38, A40;
A42: 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
A43: ( y in Y & Y in F0 ) by A41, TARSKI:def 4;
consider Fn being Element of S such that
A44: ( Y = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds
f . x = 0. ) ) by A43;
thus 0. = f . y by A43, A44; :: thesis:

end;

hence ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) ) by A6, A7, A25, A41, TARSKI:def 4; :: thesis:

end;

take x = 0. ; :: thesis:
thus ex x being Element of ExtREAL st S₃[k,x] by A42; :: thesis:

end;

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

A46: ( 1 <= k & k <= lenF ) by A38, A40, FINSEQ_1:3;
then 1 < k by A45, XXREAL_0:1;
then A47: 1 + 1 <= k by NAT_1:13;
then consider k1 being Nat such that
A48: ( k1 = k - 1 & F . k = F1 . (P2 . k1) ) by A38, A40;
( 1 <= k1 & k1 <= len P2 ) by A29, A30, A46, A47, A48, XREAL_1:11, XREAL_1:21;
then k1 in Seg (len P2) by FINSEQ_1:3;
then k1 in dom P2 by FINSEQ_1:def 3;
then P2 . k1 in (findom F1) \ N by A12, FUNCT_1:12;
then consider k' being set such that
A49: ( k' in dom F1 & F . k = F1 . k' ) by A48;
reconsider k' = k' as Element of NAT by A49;

now

per cases ;

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

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

end;

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

then consider y1 being set such that
A51: y1 in F . k by XBOOLE_0:def 1;
( F . k in rng F & rng F c= S ) by A40, FUNCT_1:12;
then ( F . k in S & S c= bool X ) ;
then reconsider y1 = y1 as Element of X by A51;
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 A49, A51, A5;
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
A52: ( 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(A39);
A53: 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 A54: ( n in dom F & x in F . n ) ; :: thesis:
then n in Seg (len F) by FINSEQ_1:def 3;
hence a . n = f . x by A52, A54; :: thesis:

end;

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

let z be set ; :: thesis:
assume z in union (rng F) ; :: thesis:
then consider Y being set such that
A55: ( z in Y & Y in rng F ) by TARSKI:def 4;
consider k being set such that
A56: ( k in dom F & Y = F . k ) by A55, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A56;

now

per cases ;

case k = 1 ; :: thesis:

then z in G1 by A38, A55, A56;
then consider Y' being set such that
A57: ( z in Y' & Y' in F0 ) by TARSKI:def 4;
consider Fn' being Element of S such that
A58: ( Y' = Fn' & Fn' in rng F1 & ( for x being Element of X st x in Fn' holds
f . x = 0. ) ) by A57;
thus z in union (rng F1) by A57, A58, TARSKI:def 4; :: thesis:

end;

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

A60: ( 1 <= k & k <= lenF ) by A38, A56, FINSEQ_1:3;
then 1 < k by A59, XXREAL_0:1;
then A61: 1 + 1 <= k by NAT_1:13;
then consider k' being Nat such that
A62: ( k' = k - 1 & F . k = F1 . (P2 . k') ) by A38, A56;
( 1 <= k' & k' <= len P2 ) by A29, A30, A60, A61, A62, XREAL_1:11, XREAL_1:21;
then k' in dom P2 by FINSEQ_3:27;
then P2 . k' in (findom F1) \ N by A12, FUNCT_1:12;
then F1 . (P2 . k') in rng F1 by FUNCT_1:12;
hence z in union (rng F1) by A55, A56, A62, TARSKI:def 4; :: thesis:

end;

end;

end;

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

end;

then A63: union (rng F) c= union (rng F1) by TARSKI:def 3;
for z being set st z in union (rng F1) holds
z in union (rng F)

let z be set ; :: thesis:
assume z in union (rng F1) ; :: thesis:
then consider Y being set such that
A64: ( z in Y & Y in rng F1 ) by TARSKI:def 4;
consider m1 being set such that
A65: ( m1 in dom F1 & Y = F1 . m1 ) by A64, FUNCT_1:def 5;
reconsider m1 = m1 as Element of NAT by A65;

now

per cases ;

case m1 in N ; :: thesis:

then consider m1' being Element of NAT such that
A66: ( m1 = m1' & m1' in dom F1 & ( for x being Element of X st x in F1 . m1' holds
f . x = 0. ) ) ;
A67: ( z in Y & Y in F0 ) by A64, A65, A66;
lenF >= 1 + 0 by A29, A30, XREAL_1:21;
then 1 in Seg lenF by FINSEQ_1:3;
then ( F . 1 in rng F & F . 1 = G1 ) by A38, FUNCT_1:12;
then ( z in union F0 & union F0 in rng F ) by A67, TARSKI:def 4;
hence z in union (rng F) by TARSKI:def 4; :: thesis:

end;

case not m1 in N ; :: thesis:

then m1 in (findom F1) \ N by A65, XBOOLE_0:def 5;
then consider m1' being set such that
A68: ( m1' in dom P2 & m1 = P2 . m1' ) by A12, FUNCT_1:def 5;
reconsider m1' = m1' as Element of NAT by A68;
m1' in Seg (len P2) by A68, FINSEQ_1:def 3;
then ( 1 <= m1' & m1' <= len P2 ) by FINSEQ_1:3;
then A69: ( 1 + 1 <= m1' + 1 & m1' + 1 <= lenF ) by A29, A30, XREAL_1:8;
reconsider m2 = m1' + 1 as Nat ;
1 <= m2 by A69, XXREAL_0:2;
then A70: m2 in Seg lenF by A69, FINSEQ_1:3;
then consider k' being Nat such that
A71: ( k' = m2 - 1 & F . m2 = F1 . (P2 . k') ) by A38, A69;
F . m2 in rng F by A38, A70, FUNCT_1:12;
hence z in union (rng F) by A64, A65, A68, A71, TARSKI:def 4; :: thesis:

end;

end;

end;

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

end;

then union (rng F1) c= union (rng F) by TARSKI:def 3;
then A72: union (rng F) = dom f by A5, A63, XBOOLE_0:def 10;
A73: ( 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 ) )

0 + 1 <= lenF by A29, A30, XREAL_1:21;
then A74: 1 in Seg lenF by FINSEQ_1:3;
then A75: 1 in Seg (len F) by A38, FINSEQ_1:def 3;
A76: F . 1 = G1 by A38, A74;
reconsider F1n0 = F1 . n0 as Element of S by A6, A7;
F1n0 in F0 by A6, A7, A8;
then x0 in F . 1 by A6, A7, A76, TARSKI:def 4;
hence a . 1 = 0. by A4, A52, A75; :: thesis:
thus dom F = dom a by A52, 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 A53; :: thesis:

end;

A77: for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n

let n be Nat; :: thesis:
assume A78: n in dom F ; :: thesis:
then ( F . n in rng F & rng F c= S ) by FUNCT_1:12;
then A79: ( F . n in S & S c= bool X ) ;
let x be set ; :: thesis:
assume A80: x in F . n ; :: thesis:
then reconsider x = x as Element of X by A79;
a . n = f . x by A53, A78, A80;
hence f . x = a . n ; :: thesis:

end;

A81: 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 A82: ( n in dom F & m in dom F & n = 1 & m <> 1 ) ; :: thesis:
then A83: F . n = G1 by A38;
( 1 <= m & m <= len F ) by A82, FINSEQ_3:27;
then 1 < m by A82, XXREAL_0:1;
then A84: ( 1 + 1 <= m & m in Seg lenF ) by A38, A82, NAT_1:13;
then consider k' being Nat such that
A85: ( k' = m - 1 & F . m = F1 . (P2 . k') ) by A38;
( m - 1 >= 1 & m <= lenF ) by A84, FINSEQ_1:3, XREAL_1:21;
then ( m - 1 >= 1 & m - 1 <= lenF - 1 ) by XREAL_1:11;
then k' in Seg (len P2) by A29, A30, A85, FINSEQ_1:3;
then k' in dom P2 by FINSEQ_1:def 3;
then P2 . k' in (findom F1) \ N by A12, FUNCT_1:12;
then A86: ( P2 . k' in dom F1 & not P2 . k' in N ) by XBOOLE_0:def 5;
(F . n) /\ (F . m) = {}

assume (F . n) /\ (F . m) <> {} ; :: thesis:
then consider v being set such that
A87: v in (F . n) /\ (F . m) by XBOOLE_0:def 1;
A88: ( v in F . n & v in F . m ) by A87, XBOOLE_0:def 4;
then consider Y being set such that
A89: ( v in Y & Y in F0 ) by A83, TARSKI:def 4;
consider Fv being Element of S such that
A90: ( Y = Fv & Fv in rng F1 & ( for x being Element of X st x in Fv holds
f . x = 0. ) ) by A89;
consider n' being set such that
A91: ( n' in dom F1 & Fv = F1 . n' ) by A90, FUNCT_1:def 5;
reconsider n' = n' as Element of NAT by A91;
n' <> P2 . k' by A86, A90, A91;
then F1 . n' misses F1 . (P2 . k') by PROB_2:def 3;
then (F1 . n') /\ (F1 . (P2 . k')) = {} by XBOOLE_0:def 7;
hence contradiction by A85, A88, A89, A90, A91, XBOOLE_0:def 4; :: thesis:

end;

hence F . n misses F . m by XBOOLE_0:def 7; :: thesis:

end;

A92: 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 A93: ( n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m ) ; :: thesis:
then A94: ( 1 <= n & n <= lenF & 1 <= m & m <= lenF ) by A38, FINSEQ_1:3;
then ( 1 < n & 1 < m ) by A93, XXREAL_0:1;
then A95: ( 1 + 1 <= n & 1 + 1 <= m ) by NAT_1:13;
then consider k1 being Nat such that
A96: ( k1 = n - 1 & F . n = F1 . (P2 . k1) ) by A38, A93;
consider k2 being Nat such that
A97: ( k2 = m - 1 & F . m = F1 . (P2 . k2) ) by A38, A93, A95;
( 1 <= n - 1 & n - 1 <= lenF - 1 & 1 <= m - 1 & m - 1 <= lenF - 1 ) by A94, A95, XREAL_1:11, XREAL_1:21;
then ( k1 in Seg (len P2) & k2 in Seg (len P2) ) by A29, A30, A96, A97, FINSEQ_1:3;
then A98: ( k1 in dom P2 & k2 in dom P2 ) by FINSEQ_1:def 3;
k1 <> k2 by A93, A96, A97;
then P2 . k1 <> P2 . k2 by A12, A98, FUNCT_1:def 8;
hence F . n misses F . m by A96, A97, PROB_2:def 3; :: thesis:

end;

for x, y being set st x <> y holds
F . x misses F . y

let x, y be set ; :: thesis:
assume A99: x <> y ; :: thesis:

now

per cases ;

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

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

now

per cases ;

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

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

end;

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

hence F . x misses F . y by A92, A99, A100; :: thesis:

end;

end;

end;

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

end;

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

now

per cases by A104;

case not x in dom F ; :: thesis:

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

end;

case not y in dom F ; :: thesis:

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

end;

end;

end;

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

end;

end;

end;

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

end;

then reconsider F = F as Finite_Sep_Sequence of S by PROB_2:def 3;
A105: for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty )

let n be Nat; :: thesis:
assume A106: ( 2 <= n & n in dom a ) ; :: thesis:
A107: f is real-valued by A1, MESFUNC2:def 5;
0 + 1 <= lenF by A29, A30, XREAL_1:21;
then A108: ( 1 in dom F & n <> 1 ) by A38, A106, FINSEQ_1:3;
then F . 1 misses F . n by A73, A81, A106;
then A109: G1 misses F . n by A38, A108;
A110: ( 1 <= n & n <= lenF ) by A38, A73, A106, FINSEQ_1:3;
consider k1 being Nat such that
A111: ( k1 = n - 1 & F . n = F1 . (P2 . k1) ) by A38, A73, A106;
1 + 1 <= n by A106;
then ( 1 <= n - 1 & n - 1 <= lenF - 1 ) by A110, XREAL_1:11, XREAL_1:21;
then k1 in Seg (len P2) by A29, A30, A111, FINSEQ_1:3;
then k1 in dom P2 by FINSEQ_1:def 3;
then P2 . k1 in (findom F1) \ N by A12, FUNCT_1:12;
then A112: F . n in rng F1 by A111, FUNCT_1:12;
( a . n <> 0. & 0. <= a . n & a . n < +infty )

per cases ;

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

then consider y being set such that
A113: y in F . n by XBOOLE_0:def 1;
A114: ( F . n in rng F & rng F c= S ) by A73, A106, FUNCT_1:12;
then ( F . n in S & S c= bool X ) ;
then reconsider y = y as Element of X by A113;
reconsider Fn = F . n as Element of S by A114;
A115: a . n = f . y by A52, A106, A113;
G1 /\ (F . n) = {} by A109, XBOOLE_0:def 7;
then A116: not y in G1 by A113, 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 A73, A106;
then Fn in F0 by A112;
hence contradiction by A113, A116, TARSKI:def 4; :: thesis:

end;

y in union (rng F) by A113, A114, TARSKI:def 4;
then ( 0. <= f . y & |.(f . y).| < +infty ) by A2, A5, A63, A107, MESFUNC2:def 1;
hence ( 0. <= a . n & a . n < +infty ) by A115, EXTREAL2:58; :: thesis:

end;

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

hence a . n <> 0. by A52, A106; :: thesis:
thus 0. <= a . n by A52, A106, S; :: thesis:
S₃[n,a . n] by A52, A106;
hence a . n < +infty by S, XXREAL_0:9; :: thesis:

end;

end;

end;

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

end;

take F ; :: thesis:
take a ; :: thesis:
thus ( 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 A72, A73, A77, A105, Def1; :: thesis: