let V be RealLinearSpace; :: thesis:
let L1, L2 be Convex_Combination of V; :: thesis:
let r be Real; :: thesis:
assume A1: ( 0 < r & r < 1 ) ; :: thesis:
then A2: r - r < 1 - r by XREAL_1:11;
then A3: r * (1 - r) > 0 by A1, XREAL_1:131;
consider F1 being FinSequence of the carrier of V such that
A4: ( F1 is one-to-one & rng F1 = Carrier L1 & ex f being FinSequence of REAL st
( len f = len F1 & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L1 . (F1 . n) & f . n >= 0 ) ) ) ) by CONVEX1:def 3;
consider f1 being FinSequence of REAL such that
A5: ( len f1 = len F1 & Sum f1 = 1 & ( for n being Nat st n in dom f1 holds
( f1 . n = L1 . (F1 . n) & f1 . n >= 0 ) ) ) by A4;
consider F2 being FinSequence of the carrier of V such that
A6: ( F2 is one-to-one & rng F2 = Carrier L2 & ex f being FinSequence of REAL st
( len f = len F2 & Sum f = 1 & ( for n being Nat st n in dom f holds
( f . n = L2 . (F2 . n) & f . n >= 0 ) ) ) ) by CONVEX1:def 3;
consider f2 being FinSequence of REAL such that
A7: ( len f2 = len F2 & Sum f2 = 1 & ( for n being Nat st n in dom f2 holds
( f2 . n = L2 . (F2 . n) & f2 . n >= 0 ) ) ) by A6;
set L = (r * L1) + ((1 - r) * L2);
A8: ( Carrier (r * L1) = Carrier L1 & Carrier ((1 - r) * L2) = Carrier L2 ) by A1, A2, RLVECT_2:65;
A9: Carrier ((r * L1) + ((1 - r) * L2)) = (Carrier (r * L1)) \/ (Carrier ((1 - r) * L2)) by A3, Lm7;
set Top = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2));
set Mid = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2));
set Btm = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1));
(Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) c= Carrier ((r * L1) + ((1 - r) * L2)) by XBOOLE_1:36;
then consider Lt being Linear_Combination of V such that
A10: Carrier Lt = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) by Lm9;
(Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) c= Carrier ((r * L1) + ((1 - r) * L2)) by A9, XBOOLE_1:29;
then consider Lm being Linear_Combination of V such that
A11: Carrier Lm = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) by Lm9;
(Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) c= Carrier ((r * L1) + ((1 - r) * L2)) by XBOOLE_1:36;
then consider Lb being Linear_Combination of V such that
A12: Carrier Lb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) by Lm9;
consider Ft being FinSequence of the carrier of V such that
A13: ( Ft is one-to-one & rng Ft = Carrier Lt & Sum Lt = Sum (Lt (#) Ft) ) by RLVECT_2:def 10;
consider Fm being FinSequence of the carrier of V such that
A14: ( Fm is one-to-one & rng Fm = Carrier Lm & Sum Lm = Sum (Lm (#) Fm) ) by RLVECT_2:def 10;
consider Fb being FinSequence of the carrier of V such that
A15: ( Fb is one-to-one & rng Fb = Carrier Lb & Sum Lb = Sum (Lb (#) Fb) ) by RLVECT_2:def 10;
deffunc H₁( set ) -> set = L1 . (Ft . $1);
consider ft being FinSequence such that
A16: ( len ft = len Ft & ( for j being Nat st j in dom ft holds
ft . j = H₁(j) ) ) from FINSEQ_1:sch 2();
rng ft c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ft ; :: thesis:
then consider x being set such that
A17: ( x in dom ft & ft . x = y ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A17;
x in Seg (len Ft) by A16, A17, FINSEQ_1:def 3;
then x in dom Ft by FINSEQ_1:def 3;
then ( Ft . x in rng Ft & rng Ft c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:12;
then reconsider Ftx = Ft . x as Element of V ;
A18: ft . x = L1 . (Ft . x) by A16, A17;
consider L1f being Function such that
A19: ( L1 = L1f & dom L1f = the carrier of V & rng L1f c= REAL ) by FUNCT_2:def 2;
Ftx in dom L1f by A19;
then ft . x in rng L1f by A18, A19, FUNCT_1:12;
hence y in REAL by A17, A19; :: thesis:

end;

then reconsider ft = ft as FinSequence of REAL by FINSEQ_1:def 4;
deffunc H₂( set ) -> set = L1 . (Fm . $1);
consider fm1 being FinSequence such that
A20: ( len fm1 = len Fm & ( for j being Nat st j in dom fm1 holds
fm1 . j = H₂(j) ) ) from FINSEQ_1:sch 2();
rng fm1 c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng fm1 ; :: thesis:
then consider x being set such that
A21: ( x in dom fm1 & fm1 . x = y ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A21;
x in Seg (len Fm) by A20, A21, FINSEQ_1:def 3;
then x in dom Fm by FINSEQ_1:def 3;
then ( Fm . x in rng Fm & rng Fm c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:12;
then reconsider Fmx = Fm . x as Element of V ;
A22: fm1 . x = L1 . (Fm . x) by A20, A21;
consider L1f being Function such that
A23: ( L1 = L1f & dom L1f = the carrier of V & rng L1f c= REAL ) by FUNCT_2:def 2;
Fmx in dom L1f by A23;
then fm1 . x in rng L1f by A22, A23, FUNCT_1:12;
hence y in REAL by A21, A23; :: thesis:

end;

then reconsider fm1 = fm1 as FinSequence of REAL by FINSEQ_1:def 4;
deffunc H₃( set ) -> set = L2 . (Fm . $1);
consider fm2 being FinSequence such that
A24: ( len fm2 = len Fm & ( for j being Nat st j in dom fm2 holds
fm2 . j = H₃(j) ) ) from FINSEQ_1:sch 2();
rng fm2 c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng fm2 ; :: thesis:
then consider x being set such that
A25: ( x in dom fm2 & fm2 . x = y ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A25;
x in Seg (len Fm) by A24, A25, FINSEQ_1:def 3;
then x in dom Fm by FINSEQ_1:def 3;
then ( Fm . x in rng Fm & rng Fm c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:12;
then reconsider Fmx = Fm . x as Element of V ;
A26: fm2 . x = L2 . (Fm . x) by A24, A25;
consider L2f being Function such that
A27: ( L2 = L2f & dom L2f = the carrier of V & rng L2f c= REAL ) by FUNCT_2:def 2;
Fmx in dom L2f by A27;
then fm2 . x in rng L2f by A26, A27, FUNCT_1:12;
hence y in REAL by A25, A27; :: thesis:

end;

then reconsider fm2 = fm2 as FinSequence of REAL by FINSEQ_1:def 4;
deffunc H₄( set ) -> set = L2 . (Fb . $1);
consider fb being FinSequence such that
A28: ( len fb = len Fb & ( for j being Nat st j in dom fb holds
fb . j = H₄(j) ) ) from FINSEQ_1:sch 2();
rng fb c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng fb ; :: thesis:
then consider x being set such that
A29: ( x in dom fb & fb . x = y ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A29;
x in Seg (len Fb) by A28, A29, FINSEQ_1:def 3;
then x in dom Fb by FINSEQ_1:def 3;
then ( Fb . x in rng Fb & rng Fb c= the carrier of V ) by FINSEQ_1:def 4, FUNCT_1:12;
then reconsider Fbx = Fb . x as Element of V ;
A30: fb . x = L2 . (Fb . x) by A28, A29;
consider L2f being Function such that
A31: ( L2 = L2f & dom L2f = the carrier of V & rng L2f c= REAL ) by FUNCT_2:def 2;
Fbx in dom L2f by A31;
then fb . x in rng L2f by A30, A31, FUNCT_1:12;
hence y in REAL by A29, A31; :: thesis:

end;

then reconsider fb = fb as FinSequence of REAL by FINSEQ_1:def 4;
A32: rng Ft misses rng Fm by A10, A11, A13, A14, XBOOLE_1:17, XBOOLE_1:85;
A33: rng Fm misses rng Fb by A11, A12, A14, A15, XBOOLE_1:17, XBOOLE_1:85;
A34: F1,Ft ^ Fm are_fiberwise_equipotent

proof

A35: Ft ^ Fm is one-to-one by A13, A14, A32, FINSEQ_3:98;
rng (Ft ^ Fm) = (rng Ft) \/ (rng Fm) by FINSEQ_1:44
.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L2)) \/ ((Carrier L1) /\ (Carrier L2)) by A3, A8, A10, A11, A13, A14, Lm7
.= (((Carrier L1) \ (Carrier L2)) \/ ((Carrier L2) \ (Carrier L2))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42
.= (((Carrier L1) \ (Carrier L2)) \/ {} ) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37
.= (Carrier L1) \ ((Carrier L2) \ (Carrier L2)) by XBOOLE_1:52
.= (Carrier L1) \ {} by XBOOLE_1:37
.= rng F1 by A4 ;
hence F1,Ft ^ Fm are_fiberwise_equipotent by A4, A35, RFINSEQ:39; :: thesis:

end;

f1,ft ^ fm1 are_fiberwise_equipotent

proof

A36: dom L1 = the carrier of V by FUNCT_2:169;
A37: for x being set holds
( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )

proof

let x be set ; :: thesis:

A38: now

assume x in dom f1 ; :: thesis:
then x in Seg (len F1) by A5, FINSEQ_1:def 3;
hence x in dom F1 by FINSEQ_1:def 3; :: thesis:
then F1 . x in rng F1 by FUNCT_1:12;
hence F1 . x in dom L1 by A4, A36; :: thesis:

end;

now

assume ( x in dom F1 & F1 . x in dom L1 ) ; :: thesis:
then x in Seg (len F1) by FINSEQ_1:def 3;
hence x in dom f1 by A5, FINSEQ_1:def 3; :: thesis:

end;

hence ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) ) by A38; :: thesis:

end;

for x being set st x in dom f1 holds
f1 . x = L1 . (F1 . x) by A5;
then A40: f1 = L1 * F1 by A37, FUNCT_1:20;
A41: rng (Ft ^ Fm) = (Carrier Lt) \/ (Carrier Lm) by A13, A14, FINSEQ_1:44;
A42: for x being set holds
( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )

proof

let x be set ; :: thesis:
A43: len (ft ^ fm1) = (len ft) + (len fm1) by FINSEQ_1:35
.= len (Ft ^ Fm) by A16, A20, FINSEQ_1:35 ;
A44: dom (ft ^ fm1) = Seg (len (ft ^ fm1)) by FINSEQ_1:def 3
.= dom (Ft ^ Fm) by A43, FINSEQ_1:def 3 ;
( x in dom (ft ^ fm1) implies (Ft ^ Fm) . x in dom L1 )

proof

assume x in dom (ft ^ fm1) ; :: thesis:
then (Ft ^ Fm) . x in rng (Ft ^ Fm) by A44, FUNCT_1:12;
then A45: (Ft ^ Fm) . x in (Carrier Lt) \/ (Carrier Lm) by A13, A14, FINSEQ_1:44;
dom L1 = the carrier of V by FUNCT_2:169;
hence (Ft ^ Fm) . x in dom L1 by A45; :: thesis:

end;

hence ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) ) by A44; :: thesis:

end;

for x being set st x in dom (ft ^ fm1) holds
(ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

proof

let x be set ; :: thesis:
assume A46: x in dom (ft ^ fm1) ; :: thesis:
then reconsider n = x as Element of NAT ;

now

per cases by A46, FINSEQ_1:38;

suppose A47: n in dom ft ; :: thesis:

then A48: n in Seg (len Ft) by A16, FINSEQ_1:def 3;
ft . n = L1 . (Ft . n) by A16, A47;
then A49: (ft ^ fm1) . n = L1 . (Ft . n) by A47, FINSEQ_1:def 7;
n in dom Ft by A48, FINSEQ_1:def 3;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A49, FINSEQ_1:def 7; :: thesis:

end;

suppose ex m being Nat st
( m in dom fm1 & n = (len ft) + m ) ; :: thesis:

then consider m being Element of NAT such that
A50: ( m in dom fm1 & n = (len ft) + m ) ;
A51: m in Seg (len Fm) by A20, A50, FINSEQ_1:def 3;
A52: (ft ^ fm1) . n = fm1 . m by A50, FINSEQ_1:def 7
.= L1 . (Fm . m) by A20, A50 ;
( m in dom Fm & n = (len Ft) + m ) by A16, A50, A51, FINSEQ_1:def 3;
hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A52, FINSEQ_1:def 7; :: thesis:

end;

hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) ; :: thesis:

end;

then A53: ft ^ fm1 = L1 * (Ft ^ Fm) by A42, FUNCT_1:20;
dom F1 = dom (Ft ^ Fm) by A34, RFINSEQ:16;
hence f1,ft ^ fm1 are_fiberwise_equipotent by A4, A34, A36, A40, A41, A53, BAGORDER:4; :: thesis:

end;

then A54: Sum f1 = Sum (ft ^ fm1) by RFINSEQ:22;
A55: F2,Fm ^ Fb are_fiberwise_equipotent

proof

A56: Fm ^ Fb is one-to-one by A14, A15, A33, FINSEQ_3:98;
rng (Fm ^ Fb) = ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1))) \/ ((Carrier (r * L1)) /\ (Carrier ((1 - r) * L2))) by A11, A12, A14, A15, FINSEQ_1:44
.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L1)) \/ ((Carrier L1) /\ (Carrier L2)) by A3, A8, Lm7
.= (((Carrier L1) \ (Carrier L1)) \/ ((Carrier L2) \ (Carrier L1))) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:42
.= (((Carrier L2) \ (Carrier L1)) \/ {} ) \/ ((Carrier L1) /\ (Carrier L2)) by XBOOLE_1:37
.= (Carrier L2) \ ((Carrier L1) \ (Carrier L1)) by XBOOLE_1:52
.= (Carrier L2) \ {} by XBOOLE_1:37
.= rng F2 by A6 ;
hence F2,Fm ^ Fb are_fiberwise_equipotent by A6, A56, RFINSEQ:39; :: thesis:

end;

f2,fm2 ^ fb are_fiberwise_equipotent

proof

A57: dom L2 = the carrier of V by FUNCT_2:169;
A58: for x being set holds
( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )

proof

let x be set ; :: thesis:

A59: now

assume x in dom f2 ; :: thesis:
then x in Seg (len F2) by A7, FINSEQ_1:def 3;
hence x in dom F2 by FINSEQ_1:def 3; :: thesis:
then F2 . x in rng F2 by FUNCT_1:12;
hence F2 . x in dom L2 by A6, A57; :: thesis:

end;

now

assume ( x in dom F2 & F2 . x in dom L2 ) ; :: thesis:
then x in Seg (len F2) by FINSEQ_1:def 3;
hence x in dom f2 by A7, FINSEQ_1:def 3; :: thesis:

end;

hence ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) ) by A59; :: thesis:

end;

for x being set st x in dom f2 holds
f2 . x = L2 . (F2 . x) by A7;
then A61: f2 = L2 * F2 by A58, FUNCT_1:20;
A62: rng (Fm ^ Fb) = (Carrier Lm) \/ (Carrier Lb) by A14, A15, FINSEQ_1:44;
A63: for x being set holds
( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )

proof

let x be set ; :: thesis:
A64: len (fm2 ^ fb) = (len fm2) + (len fb) by FINSEQ_1:35
.= len (Fm ^ Fb) by A24, A28, FINSEQ_1:35 ;
A65: dom (fm2 ^ fb) = Seg (len (fm2 ^ fb)) by FINSEQ_1:def 3
.= dom (Fm ^ Fb) by A64, FINSEQ_1:def 3 ;
( x in dom (fm2 ^ fb) implies (Fm ^ Fb) . x in dom L2 )

proof

assume x in dom (fm2 ^ fb) ; :: thesis:
then (Fm ^ Fb) . x in rng (Fm ^ Fb) by A65, FUNCT_1:12;
then A66: (Fm ^ Fb) . x in (Carrier Lm) \/ (Carrier Lb) by A14, A15, FINSEQ_1:44;
dom L2 = the carrier of V by FUNCT_2:169;
hence (Fm ^ Fb) . x in dom L2 by A66; :: thesis:

end;

hence ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) ) by A65; :: thesis:

end;

for x being set st x in dom (fm2 ^ fb) holds
(fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

proof

let x be set ; :: thesis:
assume A67: x in dom (fm2 ^ fb) ; :: thesis:
then reconsider n = x as Element of NAT ;

now

per cases by A67, FINSEQ_1:38;

suppose A68: n in dom fm2 ; :: thesis:

then A69: n in Seg (len Fm) by A24, FINSEQ_1:def 3;
fm2 . n = L2 . (Fm . n) by A24, A68;
then A70: (fm2 ^ fb) . n = L2 . (Fm . n) by A68, FINSEQ_1:def 7;
n in dom Fm by A69, FINSEQ_1:def 3;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A70, FINSEQ_1:def 7; :: thesis:

end;

suppose ex m being Nat st
( m in dom fb & n = (len fm2) + m ) ; :: thesis:

then consider m being Element of NAT such that
A71: ( m in dom fb & n = (len fm2) + m ) ;
A72: m in Seg (len Fb) by A28, A71, FINSEQ_1:def 3;
A73: (fm2 ^ fb) . n = fb . m by A71, FINSEQ_1:def 7
.= L2 . (Fb . m) by A28, A71 ;
( m in dom Fb & n = (len Fm) + m ) by A24, A71, A72, FINSEQ_1:def 3;
hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A73, FINSEQ_1:def 7; :: thesis:

end;

hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) ; :: thesis:

end;

then A74: fm2 ^ fb = L2 * (Fm ^ Fb) by A63, FUNCT_1:20;
dom F2 = dom (Fm ^ Fb) by A55, RFINSEQ:16;
hence f2,fm2 ^ fb are_fiberwise_equipotent by A6, A55, A57, A61, A62, A74, BAGORDER:4; :: thesis:

end;

then A75: Sum f2 = Sum (fm2 ^ fb) by RFINSEQ:22;
set F = (Ft ^ Fm) ^ Fb;
set f = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb);
A76: rng (Ft ^ Fm) = Carrier L1 by A4, A34, CLASSES1:83;
A77: rng Fb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1) by A1, A12, A15, RLVECT_2:65;
then A78: rng (Ft ^ Fm) misses rng Fb by A76, XBOOLE_1:79;
Ft ^ Fm is one-to-one by A13, A14, A32, FINSEQ_3:98;
then A79: (Ft ^ Fm) ^ Fb is one-to-one by A15, A78, FINSEQ_3:98;
A80: rng ((Ft ^ Fm) ^ Fb) = (Carrier L1) \/ ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1)) by A76, A77, FINSEQ_1:44
.= (Carrier L1) \/ (Carrier ((r * L1) + ((1 - r) * L2))) by XBOOLE_1:39
.= Carrier ((r * L1) + ((1 - r) * L2)) by A8, A9, XBOOLE_1:7, XBOOLE_1:12 ;
( len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) & Sum (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = 1 & ( for n being Nat st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ) )

proof

A81: len (r * fm1) = len fm1 by EUCLID_2:8
.= len ((1 - r) * fm2) by A20, A24, EUCLID_2:8 ;
len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:35
.= ((len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:35
.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by EUCLID_2:8
.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len fb) by EUCLID_2:8
.= ((len ft) + (len (r * fm1))) + (len fb) by A81, INTEGRA5:2
.= ((len Ft) + (len Fm)) + (len Fb) by A16, A20, A28, EUCLID_2:8
.= (len (Ft ^ Fm)) + (len Fb) by FINSEQ_1:35 ;
hence len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) by FINSEQ_1:35; :: thesis:
Sum (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = (Sum ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:105
.= ((Sum (r * ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:105
.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:117
.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:117
.= ((r * (Sum ft)) + ((Sum (r * fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by A81, INTEGRA5:2
.= ((r * (Sum ft)) + ((r * (Sum fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:117
.= ((r * (Sum ft)) + ((r * (Sum fm1)) + ((1 - r) * (Sum fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:117
.= (r * ((Sum ft) + (Sum fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb)))
.= (r * (Sum (ft ^ fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) by RVSUM_1:105
.= (r * 1) + ((1 - r) * 1) by A5, A7, A54, A75, RVSUM_1:105
.= 0 + 1 ;
hence Sum (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = 1 ; :: thesis:
for n being Element of NAT st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 )

proof

let n be Element of NAT ; :: thesis:
assume A82: n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) ; :: thesis:

now

per cases by A82, FINSEQ_1:38;

suppose A83: n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ; :: thesis:

then A84: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) . n by FINSEQ_1:def 7;

now

per cases by A83, FINSEQ_1:38;

suppose A85: n in dom (r * ft) ; :: thesis:

then A86: n in dom ft by VALUED_1:def 5;
then A87: n in Seg (len Ft) by A16, FINSEQ_1:def 3;
A88: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = (r * ft) . n by A84, A85, FINSEQ_1:def 7
.= r * (ft . n) by RVSUM_1:66
.= r * (L1 . (Ft . n)) by A16, A86 ;
A89: n in dom Ft by A87, FINSEQ_1:def 3;
then A90: Ft . n in rng Ft by FUNCT_1:12;
A91: Ft . n in Carrier Lt by A13, A89, FUNCT_1:12;
then reconsider Ftn = Ft . n as Element of V ;
( Ft . n in Carrier ((r * L1) + ((1 - r) * L2)) & not Ft . n in Carrier L2 ) by A8, A10, A91, XBOOLE_0:def 5;
then L2 . Ftn = 0 by RLVECT_2:28;
then (1 - r) * (L2 . Ftn) = 0 ;
then ((1 - r) * L2) . Ftn = 0 by RLVECT_2:def 13;
then A92: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Ftn) + (((1 - r) * L2) . Ftn) by A88, RLVECT_2:def 13
.= ((r * L1) + ((1 - r) * L2)) . (Ft . n) by RLVECT_2:def 12 ;
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:35
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by EUCLID_2:8
.= (len ft) + (len (r * fm1)) by A81, INTEGRA5:2
.= (len Ft) + (len Fm) by A16, A20, EUCLID_2:8
.= len (Ft ^ Fm) by FINSEQ_1:35 ;
then n in Seg (len (Ft ^ Fm)) by A83, FINSEQ_1:def 3;
then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;
then (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A89, A92, FINSEQ_1:def 7; :: thesis:
rng Ft c= rng (Ft ^ Fm) by FINSEQ_1:42;
then Ft . n in rng (Ft ^ Fm) by A90;
then Ft . n in rng F1 by A34, CLASSES1:83;
then consider m' being set such that
A93: ( m' in dom F1 & F1 . m' = Ft . n ) by FUNCT_1:def 5;
reconsider m' = m' as Element of NAT by A93;
m' in Seg (len f1) by A5, A93, FINSEQ_1:def 3;
then m' in dom f1 by FINSEQ_1:def 3;
then ( f1 . m' = L1 . (F1 . m') & f1 . m' >= 0 ) by A5;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A1, A88, A93, XREAL_1:129; :: thesis:

end;

suppose ex k being Nat st
( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ; :: thesis:

then consider m being Element of NAT such that
A94: ( m in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + m ) ;
len (r * fm1) = len fm1 by EUCLID_2:8
.= len ((1 - r) * fm2) by A20, A24, EUCLID_2:8 ;
then len ((r * fm1) + ((1 - r) * fm2)) = len (r * fm1) by INTEGRA5:2
.= len fm1 by EUCLID_2:8 ;
then A95: m in dom fm1 by A94, FINSEQ_3:31;
then A96: m in dom fm2 by A20, A24, FINSEQ_3:31;
A97: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * fm1) + ((1 - r) * fm2)) . m by A84, A94, FINSEQ_1:def 7
.= ((r * fm1) . m) + (((1 - r) * fm2) . m) by A94, VALUED_1:def 1
.= (r * (fm1 . m)) + (((1 - r) * fm2) . m) by RVSUM_1:66
.= (r * (fm1 . m)) + ((1 - r) * (fm2 . m)) by RVSUM_1:66
.= (r * (L1 . (Fm . m))) + ((1 - r) * (fm2 . m)) by A20, A95
.= (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) by A24, A96 ;
A98: m in dom Fm by A96, A24, FINSEQ_3:31;
then A99: Fm . m in rng Fm by FUNCT_1:12;
then reconsider Fmm = Fm . m as Element of V by A14;
( r * (L1 . Fmm) = (r * L1) . (Fm . m) & (1 - r) * (L2 . Fmm) = ((1 - r) * L2) . (Fm . m) ) by RLVECT_2:def 13;
then A100: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (Fm . m) by A97, RLVECT_2:def 12;
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:35
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by EUCLID_2:8
.= (len ft) + (len (r * fm1)) by A81, INTEGRA5:2
.= (len Ft) + (len Fm) by A16, A20, EUCLID_2:8
.= len (Ft ^ Fm) by FINSEQ_1:35 ;
then n in Seg (len (Ft ^ Fm)) by A83, FINSEQ_1:def 3;
then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;
then A101: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;
len (r * ft) = len Ft by A16, EUCLID_2:8;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A94, A98, A100, A101, FINSEQ_1:def 7; :: thesis:
rng Fm c= rng (Ft ^ Fm) by FINSEQ_1:43;
then Fm . m in rng (Ft ^ Fm) by A99;
then Fm . m in rng F1 by A34, CLASSES1:83;
then consider m' being set such that
A102: ( m' in dom F1 & F1 . m' = Fm . m ) by FUNCT_1:def 5;
reconsider m' = m' as Element of NAT by A102;
m' in Seg (len F1) by A102, FINSEQ_1:def 3;
then m' in dom f1 by A5, FINSEQ_1:def 3;
then ( f1 . m' = L1 . (F1 . m') & f1 . m' >= 0 ) by A5;
then A103: r * (L1 . (Fm . m)) >= 0 by A1, A102, XREAL_1:129;
rng Fm c= rng (Fm ^ Fb) by FINSEQ_1:42;
then Fm . m in rng (Fm ^ Fb) by A99;
then Fm . m in rng F2 by A55, CLASSES1:83;
then consider m' being set such that
A104: ( m' in dom F2 & F2 . m' = Fm . m ) by FUNCT_1:def 5;
reconsider m' = m' as Element of NAT by A104;
m' in Seg (len F2) by A104, FINSEQ_1:def 3;
then m' in dom f2 by A7, FINSEQ_1:def 3;
then ( f2 . m' = L2 . (F2 . m') & f2 . m' >= 0 ) by A7;
then (1 - r) * (L2 . (Fm . m)) >= 0 by A2, A104, XREAL_1:129;
then (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) >= 0 + 0 by A103, XREAL_1:9;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A97; :: thesis:

end;

hence ( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; :: thesis:

end;

suppose ex m being Nat st
( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ; :: thesis:

then consider m being Element of NAT such that
A105: ( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ;
A106: m in dom fb by A105, VALUED_1:def 5;
then A107: m in Seg (len Fb) by A28, FINSEQ_1:def 3;
A108: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((1 - r) * fb) . m by A105, FINSEQ_1:def 7
.= (1 - r) * (fb . m) by RVSUM_1:66
.= (1 - r) * (L2 . (Fb . m)) by A28, A106 ;
A109: m in dom Fb by A107, FINSEQ_1:def 3;
then A110: Fb . m in rng Fb by FUNCT_1:12;
then reconsider Fbm = Fb . m as Element of V by A15;
( Fb . m in Carrier ((r * L1) + ((1 - r) * L2)) & not Fb . m in Carrier L1 ) by A8, A12, A15, A110, XBOOLE_0:def 5;
then L1 . Fbm = 0 by RLVECT_2:28;
then r * (L1 . Fbm) = 0 ;
then (r * L1) . Fbm = 0 by RLVECT_2:def 13;
then A111: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Fbm) + (((1 - r) * L2) . Fbm) by A108, RLVECT_2:def 13
.= ((r * L1) + ((1 - r) * L2)) . (Fb . m) by RLVECT_2:def 12 ;
len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:35
.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by EUCLID_2:8
.= (len ft) + (len (r * fm1)) by A81, INTEGRA5:2
.= (len Ft) + (len Fm) by A16, A20, EUCLID_2:8
.= len (Ft ^ Fm) by FINSEQ_1:35 ;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A105, A109, A111, FINSEQ_1:def 7; :: thesis:
rng Fb c= rng (Fm ^ Fb) by FINSEQ_1:43;
then Fb . m in rng (Fm ^ Fb) by A110;
then Fb . m in rng F2 by A55, CLASSES1:83;
then consider m' being set such that
A112: ( m' in dom F2 & F2 . m' = Fb . m ) by FUNCT_1:def 5;
reconsider m' = m' as Element of NAT by A112;
m' in Seg (len F2) by A112, FINSEQ_1:def 3;
then m' in dom f2 by A7, FINSEQ_1:def 3;
then ( f2 . m' = L2 . (F2 . m') & f2 . m' >= 0 ) by A7;
hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A2, A108, A112, XREAL_1:129; :: thesis:

end;

hence for n being Nat st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
( (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) & (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 ) ; :: thesis:

end;

hence (r * L1) + ((1 - r) * L2) is Convex_Combination of V by A79, A80, CONVEX1:def 3; :: thesis: