let V be RealLinearSpace; :: thesis: for L1, L2 being Convex_Combination of V

for r being Real st 0 < r & r < 1 holds

(r * L1) + ((1 - r) * L2) is Convex_Combination of V

let L1, L2 be Convex_Combination of V; :: thesis: for r being Real st 0 < r & r < 1 holds

(r * L1) + ((1 - r) * L2) is Convex_Combination of V

let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of V )

assume that

A1: 0 < r and

A2: r < 1 ; :: thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of V

A3: Carrier (r * L1) = Carrier L1 by A1, RLVECT_2:42;

set Mid = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2));

set L = (r * L1) + ((1 - r) * L2);

consider F2 being FinSequence of the carrier of V such that

A4: F2 is one-to-one and

A5: rng F2 = Carrier L2 and

A6: 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;

set Btm = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1));

set Top = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2));

consider F1 being FinSequence of the carrier of V such that

A7: F1 is one-to-one and

A8: rng F1 = Carrier L1 and

A9: 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 Lt being Linear_Combination of V such that

A10: Carrier Lt = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:36;

A11: r - r < 1 - r by A2, XREAL_1:9;

then A12: Carrier ((1 - r) * L2) = Carrier L2 by RLVECT_2:42;

A13: r * (1 - r) > 0 by A1, A11, XREAL_1:129;

then A14: Carrier ((r * L1) + ((1 - r) * L2)) = (Carrier (r * L1)) \/ (Carrier ((1 - r) * L2)) by Lm5;

then consider Lm being Linear_Combination of V such that

A15: Carrier Lm = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:29;

consider Lb being Linear_Combination of V such that

A16: Carrier Lb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) by Lm7, XBOOLE_1:36;

consider Ft being FinSequence of the carrier of V such that

A17: Ft is one-to-one and

A18: rng Ft = Carrier Lt and

Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;

consider Fb being FinSequence of the carrier of V such that

A19: Fb is one-to-one and

A20: rng Fb = Carrier Lb and

Sum Lb = Sum (Lb (#) Fb) by RLVECT_2:def 8;

consider Fm being FinSequence of the carrier of V such that

A21: Fm is one-to-one and

A22: rng Fm = Carrier Lm and

Sum Lm = Sum (Lm (#) Fm) by RLVECT_2:def 8;

A23: rng (Ft ^ Fm) = (rng Ft) \/ (rng Fm) by FINSEQ_1:31

.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L2)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, A10, A15, A18, A22, Lm5

.= (((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 A8 ;

A24: rng Ft misses rng Fm by A10, A15, A18, A22, XBOOLE_1:17, XBOOLE_1:85;

then A25: Ft ^ Fm is one-to-one by A17, A21, FINSEQ_3:91;

set F = (Ft ^ Fm) ^ Fb;

consider f2 being FinSequence of REAL such that

A26: len f2 = len F2 and

A27: Sum f2 = 1 and

A28: for n being Nat st n in dom f2 holds

( f2 . n = L2 . (F2 . n) & f2 . n >= 0 ) by A6;

deffunc H_{1}( set ) -> set = L1 . (Ft . $1);

consider ft being FinSequence such that

A29: ( len ft = len Ft & ( for j being Nat st j in dom ft holds

ft . j = H_{1}(j) ) )
from FINSEQ_1:sch 2();

rng ft c= REAL

deffunc H_{2}( set ) -> set = L1 . (Fm . $1);

consider fm1 being FinSequence such that

A37: ( len fm1 = len Fm & ( for j being Nat st j in dom fm1 holds

fm1 . j = H_{2}(j) ) )
from FINSEQ_1:sch 2();

rng fm1 c= REAL

deffunc H_{3}( set ) -> set = L2 . (Fm . $1);

consider fm2 being FinSequence such that

A45: ( len fm2 = len Fm & ( for j being Nat st j in dom fm2 holds

fm2 . j = H_{3}(j) ) )
from FINSEQ_1:sch 2();

A46: for x being object st x in dom (ft ^ fm1) holds

(ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )

A57: dom L2 = the carrier of V by FUNCT_2:92;

A58: for x being object holds

( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )_{4}( set ) -> set = L2 . (Fb . $1);

consider fb being FinSequence such that

A61: ( len fb = len Fb & ( for j being Nat st j in dom fb holds

fb . j = H_{4}(j) ) )
from FINSEQ_1:sch 2();

rng fm2 c= REAL

A69: len (r * fm1) = len fm1 by RVSUM_1:117

.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;

rng fb c= REAL

set f = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb);

consider f1 being FinSequence of REAL such that

A77: len f1 = len F1 and

A78: Sum f1 = 1 and

A79: for n being Nat st n in dom f1 holds

( f1 . n = L1 . (F1 . n) & f1 . n >= 0 ) by A9;

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:22

.= ((len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22

.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by RVSUM_1:117

.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len fb) by RVSUM_1:117

.= ((len ft) + (len (r * fm1))) + (len fb) by A69, INTEGRA5:2

.= ((len Ft) + (len Fm)) + (len Fb) by A29, A37, A61, RVSUM_1:117

.= (len (Ft ^ Fm)) + (len Fb) by FINSEQ_1:22 ;

then A80: len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) by FINSEQ_1:22;

A81: dom L1 = the carrier of V by FUNCT_2:92;

A82: for x being object holds

( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )

for x being object st x in dom f1 holds

f1 . x = L1 . (F1 . x) by A79;

then A86: f1 = L1 * F1 by A82, FUNCT_1:10;

Ft ^ Fm is one-to-one by A17, A21, A24, FINSEQ_3:91;

then A87: F1,Ft ^ Fm are_fiberwise_equipotent by A7, A23, RFINSEQ:26;

then dom F1 = dom (Ft ^ Fm) by RFINSEQ:3;

then A88: Sum f1 = Sum (ft ^ fm1) by A8, A87, A81, A86, A85, A56, CLASSES1:83, RFINSEQ:9;

A89: rng (Fm ^ Fb) = (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;

for x being object st x in dom f2 holds

f2 . x = L2 . (F2 . x) by A28;

then A90: f2 = L2 * F2 by A58, FUNCT_1:10;

A91: rng (Fm ^ Fb) = ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1))) \/ ((Carrier (r * L1)) /\ (Carrier ((1 - r) * L2))) by A15, A16, A22, A20, FINSEQ_1:31

.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L1)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, Lm5

.= (((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 A5 ;

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 )

( (((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 ) ;

A129: rng Fb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1) by A1, A16, A20, RLVECT_2:42;

then rng (Ft ^ Fm) misses rng Fb by A8, A23, XBOOLE_1:79;

then A130: (Ft ^ Fm) ^ Fb is one-to-one by A19, A25, FINSEQ_3:91;

A131: for x being object st x in dom (fm2 ^ fb) holds

(fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )

rng Fm misses rng Fb by A15, A16, A22, A20, XBOOLE_1:17, XBOOLE_1:85;

then Fm ^ Fb is one-to-one by A21, A19, FINSEQ_3:91;

then A142: F2,Fm ^ Fb are_fiberwise_equipotent by A4, A91, RFINSEQ:26;

then dom F2 = dom (Fm ^ Fb) by RFINSEQ:3;

then A143: Sum f2 = Sum (fm2 ^ fb) by A5, A142, A57, A90, A89, A141, CLASSES1:83, RFINSEQ:9;

A144: 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:75

.= ((Sum (r * ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75

.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:87

.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87

.= ((r * (Sum ft)) + ((Sum (r * fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by A69, INTEGRA5:2

.= ((r * (Sum ft)) + ((r * (Sum fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87

.= ((r * (Sum ft)) + ((r * (Sum fm1)) + ((1 - r) * (Sum fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87

.= (r * ((Sum ft) + (Sum fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb)))

.= (r * (Sum (ft ^ fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) by RVSUM_1:75

.= (r * 1) + ((1 - r) * 1) by A78, A27, A88, A143, RVSUM_1:75

.= 0 + 1 ;

rng ((Ft ^ Fm) ^ Fb) = (Carrier L1) \/ ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1)) by A8, A23, A129, FINSEQ_1:31

.= (Carrier L1) \/ (Carrier ((r * L1) + ((1 - r) * L2))) by XBOOLE_1:39

.= Carrier ((r * L1) + ((1 - r) * L2)) by A3, A14, XBOOLE_1:7, XBOOLE_1:12 ;

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

for r being Real st 0 < r & r < 1 holds

(r * L1) + ((1 - r) * L2) is Convex_Combination of V

let L1, L2 be Convex_Combination of V; :: thesis: for r being Real st 0 < r & r < 1 holds

(r * L1) + ((1 - r) * L2) is Convex_Combination of V

let r be Real; :: thesis: ( 0 < r & r < 1 implies (r * L1) + ((1 - r) * L2) is Convex_Combination of V )

assume that

A1: 0 < r and

A2: r < 1 ; :: thesis: (r * L1) + ((1 - r) * L2) is Convex_Combination of V

A3: Carrier (r * L1) = Carrier L1 by A1, RLVECT_2:42;

set Mid = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2));

set L = (r * L1) + ((1 - r) * L2);

consider F2 being FinSequence of the carrier of V such that

A4: F2 is one-to-one and

A5: rng F2 = Carrier L2 and

A6: 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;

set Btm = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1));

set Top = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2));

consider F1 being FinSequence of the carrier of V such that

A7: F1 is one-to-one and

A8: rng F1 = Carrier L1 and

A9: 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 Lt being Linear_Combination of V such that

A10: Carrier Lt = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:36;

A11: r - r < 1 - r by A2, XREAL_1:9;

then A12: Carrier ((1 - r) * L2) = Carrier L2 by RLVECT_2:42;

A13: r * (1 - r) > 0 by A1, A11, XREAL_1:129;

then A14: Carrier ((r * L1) + ((1 - r) * L2)) = (Carrier (r * L1)) \/ (Carrier ((1 - r) * L2)) by Lm5;

then consider Lm being Linear_Combination of V such that

A15: Carrier Lm = (Carrier (r * L1)) /\ (Carrier ((1 - r) * L2)) by Lm7, XBOOLE_1:29;

consider Lb being Linear_Combination of V such that

A16: Carrier Lb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1)) by Lm7, XBOOLE_1:36;

consider Ft being FinSequence of the carrier of V such that

A17: Ft is one-to-one and

A18: rng Ft = Carrier Lt and

Sum Lt = Sum (Lt (#) Ft) by RLVECT_2:def 8;

consider Fb being FinSequence of the carrier of V such that

A19: Fb is one-to-one and

A20: rng Fb = Carrier Lb and

Sum Lb = Sum (Lb (#) Fb) by RLVECT_2:def 8;

consider Fm being FinSequence of the carrier of V such that

A21: Fm is one-to-one and

A22: rng Fm = Carrier Lm and

Sum Lm = Sum (Lm (#) Fm) by RLVECT_2:def 8;

A23: rng (Ft ^ Fm) = (rng Ft) \/ (rng Fm) by FINSEQ_1:31

.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L2)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, A10, A15, A18, A22, Lm5

.= (((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 A8 ;

A24: rng Ft misses rng Fm by A10, A15, A18, A22, XBOOLE_1:17, XBOOLE_1:85;

then A25: Ft ^ Fm is one-to-one by A17, A21, FINSEQ_3:91;

set F = (Ft ^ Fm) ^ Fb;

consider f2 being FinSequence of REAL such that

A26: len f2 = len F2 and

A27: Sum f2 = 1 and

A28: for n being Nat st n in dom f2 holds

( f2 . n = L2 . (F2 . n) & f2 . n >= 0 ) by A6;

deffunc H

consider ft being FinSequence such that

A29: ( len ft = len Ft & ( for j being Nat st j in dom ft holds

ft . j = H

rng ft c= REAL

proof

then reconsider ft = ft as FinSequence of REAL by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ft or y in REAL )

consider L1f being Function such that

A30: L1 = L1f and

A31: dom L1f = the carrier of V and

A32: rng L1f c= REAL by FUNCT_2:def 2;

assume y in rng ft ; :: thesis: y in REAL

then consider x being object such that

A33: x in dom ft and

A34: ft . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A33;

A35: ft . x = L1 . (Ft . x) by A29, A33;

x in Seg (len Ft) by A29, A33, FINSEQ_1:def 3;

then x in dom Ft by FINSEQ_1:def 3;

then A36: Ft . x in rng Ft by FUNCT_1:3;

rng Ft c= the carrier of V by FINSEQ_1:def 4;

then reconsider Ftx = Ft . x as Element of V by A36;

Ftx in dom L1f by A31;

then ft . x in rng L1f by A35, A30, FUNCT_1:3;

hence y in REAL by A34, A32; :: thesis: verum

end;consider L1f being Function such that

A30: L1 = L1f and

A31: dom L1f = the carrier of V and

A32: rng L1f c= REAL by FUNCT_2:def 2;

assume y in rng ft ; :: thesis: y in REAL

then consider x being object such that

A33: x in dom ft and

A34: ft . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A33;

A35: ft . x = L1 . (Ft . x) by A29, A33;

x in Seg (len Ft) by A29, A33, FINSEQ_1:def 3;

then x in dom Ft by FINSEQ_1:def 3;

then A36: Ft . x in rng Ft by FUNCT_1:3;

rng Ft c= the carrier of V by FINSEQ_1:def 4;

then reconsider Ftx = Ft . x as Element of V by A36;

Ftx in dom L1f by A31;

then ft . x in rng L1f by A35, A30, FUNCT_1:3;

hence y in REAL by A34, A32; :: thesis: verum

deffunc H

consider fm1 being FinSequence such that

A37: ( len fm1 = len Fm & ( for j being Nat st j in dom fm1 holds

fm1 . j = H

rng fm1 c= REAL

proof

then reconsider fm1 = fm1 as FinSequence of REAL by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fm1 or y in REAL )

consider L1f being Function such that

A38: L1 = L1f and

A39: dom L1f = the carrier of V and

A40: rng L1f c= REAL by FUNCT_2:def 2;

assume y in rng fm1 ; :: thesis: y in REAL

then consider x being object such that

A41: x in dom fm1 and

A42: fm1 . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A41;

A43: fm1 . x = L1 . (Fm . x) by A37, A41;

x in Seg (len Fm) by A37, A41, FINSEQ_1:def 3;

then x in dom Fm by FINSEQ_1:def 3;

then A44: Fm . x in rng Fm by FUNCT_1:3;

rng Fm c= the carrier of V by FINSEQ_1:def 4;

then reconsider Fmx = Fm . x as Element of V by A44;

Fmx in dom L1f by A39;

then fm1 . x in rng L1f by A43, A38, FUNCT_1:3;

hence y in REAL by A42, A40; :: thesis: verum

end;consider L1f being Function such that

A38: L1 = L1f and

A39: dom L1f = the carrier of V and

A40: rng L1f c= REAL by FUNCT_2:def 2;

assume y in rng fm1 ; :: thesis: y in REAL

then consider x being object such that

A41: x in dom fm1 and

A42: fm1 . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A41;

A43: fm1 . x = L1 . (Fm . x) by A37, A41;

x in Seg (len Fm) by A37, A41, FINSEQ_1:def 3;

then x in dom Fm by FINSEQ_1:def 3;

then A44: Fm . x in rng Fm by FUNCT_1:3;

rng Fm c= the carrier of V by FINSEQ_1:def 4;

then reconsider Fmx = Fm . x as Element of V by A44;

Fmx in dom L1f by A39;

then fm1 . x in rng L1f by A43, A38, FUNCT_1:3;

hence y in REAL by A42, A40; :: thesis: verum

deffunc H

consider fm2 being FinSequence such that

A45: ( len fm2 = len Fm & ( for j being Nat st j in dom fm2 holds

fm2 . j = H

A46: for x being object st x in dom (ft ^ fm1) holds

(ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

proof

for x being object holds
let x be object ; :: thesis: ( x in dom (ft ^ fm1) implies (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) )

assume A47: x in dom (ft ^ fm1) ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

then reconsider n = x as Element of NAT ;

end;assume A47: x in dom (ft ^ fm1) ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

then reconsider n = x as Element of NAT ;

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

hence
(ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)
; :: thesis: verumper cases
( n in dom ft or ex m being Nat st

( m in dom fm1 & n = (len ft) + m ) ) by A47, FINSEQ_1:25;

end;

( m in dom fm1 & n = (len ft) + m ) ) by A47, FINSEQ_1:25;

suppose A48:
n in dom ft
; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

then
n in Seg (len Ft)
by A29, FINSEQ_1:def 3;

then A49: n in dom Ft by FINSEQ_1:def 3;

ft . n = L1 . (Ft . n) by A29, A48;

then (ft ^ fm1) . n = L1 . (Ft . n) by A48, FINSEQ_1:def 7;

hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A49, FINSEQ_1:def 7; :: thesis: verum

end;then A49: n in dom Ft by FINSEQ_1:def 3;

ft . n = L1 . (Ft . n) by A29, A48;

then (ft ^ fm1) . n = L1 . (Ft . n) by A48, FINSEQ_1:def 7;

hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A49, FINSEQ_1:def 7; :: thesis: verum

suppose
ex m being Nat st

( m in dom fm1 & n = (len ft) + m ) ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

( m in dom fm1 & n = (len ft) + m ) ; :: thesis: (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x)

then consider m being Element of NAT such that

A50: m in dom fm1 and

A51: n = (len ft) + m ;

m in Seg (len Fm) by A37, A50, FINSEQ_1:def 3;

then A52: m in dom Fm by FINSEQ_1:def 3;

(ft ^ fm1) . n = fm1 . m by A50, A51, FINSEQ_1:def 7

.= L1 . (Fm . m) by A37, A50 ;

hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A29, A51, A52, FINSEQ_1:def 7; :: thesis: verum

end;A50: m in dom fm1 and

A51: n = (len ft) + m ;

m in Seg (len Fm) by A37, A50, FINSEQ_1:def 3;

then A52: m in dom Fm by FINSEQ_1:def 3;

(ft ^ fm1) . n = fm1 . m by A50, A51, FINSEQ_1:def 7

.= L1 . (Fm . m) by A37, A50 ;

hence (ft ^ fm1) . x = L1 . ((Ft ^ Fm) . x) by A29, A51, A52, FINSEQ_1:def 7; :: thesis: verum

( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )

proof

then A56:
ft ^ fm1 = L1 * (Ft ^ Fm)
by A46, FUNCT_1:10;
let x be object ; :: thesis: ( x in dom (ft ^ fm1) iff ( x in dom (Ft ^ Fm) & (Ft ^ Fm) . x in dom L1 ) )

A53: len (ft ^ fm1) = (len ft) + (len fm1) by FINSEQ_1:22

.= len (Ft ^ Fm) by A29, A37, FINSEQ_1:22 ;

A54: dom (ft ^ fm1) = Seg (len (ft ^ fm1)) by FINSEQ_1:def 3

.= dom (Ft ^ Fm) by A53, FINSEQ_1:def 3 ;

( x in dom (ft ^ fm1) implies (Ft ^ Fm) . x in dom L1 )

end;A53: len (ft ^ fm1) = (len ft) + (len fm1) by FINSEQ_1:22

.= len (Ft ^ Fm) by A29, A37, FINSEQ_1:22 ;

A54: dom (ft ^ fm1) = Seg (len (ft ^ fm1)) by FINSEQ_1:def 3

.= dom (Ft ^ Fm) by A53, FINSEQ_1:def 3 ;

( x in dom (ft ^ fm1) implies (Ft ^ Fm) . x in dom L1 )

proof

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

then (Ft ^ Fm) . x in rng (Ft ^ Fm) by A54, FUNCT_1:3;

then A55: (Ft ^ Fm) . x in (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31;

dom L1 = the carrier of V by FUNCT_2:92;

hence (Ft ^ Fm) . x in dom L1 by A55; :: thesis: verum

end;then (Ft ^ Fm) . x in rng (Ft ^ Fm) by A54, FUNCT_1:3;

then A55: (Ft ^ Fm) . x in (Carrier Lt) \/ (Carrier Lm) by A18, A22, FINSEQ_1:31;

dom L1 = the carrier of V by FUNCT_2:92;

hence (Ft ^ Fm) . x in dom L1 by A55; :: thesis: verum

A57: dom L2 = the carrier of V by FUNCT_2:92;

A58: for x being object holds

( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )

proof

deffunc H
let x be object ; :: thesis: ( x in dom f2 iff ( x in dom F2 & F2 . x in dom L2 ) )

end;A59: now :: thesis: ( x in dom f2 implies ( x in dom F2 & F2 . x in dom L2 ) )

assume
x in dom f2
; :: thesis: ( x in dom F2 & F2 . x in dom L2 )

then x in Seg (len F2) by A26, FINSEQ_1:def 3;

hence x in dom F2 by FINSEQ_1:def 3; :: thesis: F2 . x in dom L2

then F2 . x in rng F2 by FUNCT_1:3;

hence F2 . x in dom L2 by A5, A57; :: thesis: verum

end;then x in Seg (len F2) by A26, FINSEQ_1:def 3;

hence x in dom F2 by FINSEQ_1:def 3; :: thesis: F2 . x in dom L2

then F2 . x in rng F2 by FUNCT_1:3;

hence F2 . x in dom L2 by A5, A57; :: thesis: verum

now :: thesis: ( x in dom F2 & F2 . x in dom L2 implies x in dom f2 )

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

A60: x in dom F2 and

F2 . x in dom L2 ; :: thesis: x in dom f2

x in Seg (len F2) by A60, FINSEQ_1:def 3;

hence x in dom f2 by A26, FINSEQ_1:def 3; :: thesis: verum

end;A60: x in dom F2 and

F2 . x in dom L2 ; :: thesis: x in dom f2

x in Seg (len F2) by A60, FINSEQ_1:def 3;

hence x in dom f2 by A26, FINSEQ_1:def 3; :: thesis: verum

consider fb being FinSequence such that

A61: ( len fb = len Fb & ( for j being Nat st j in dom fb holds

fb . j = H

rng fm2 c= REAL

proof

then reconsider fm2 = fm2 as FinSequence of REAL by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fm2 or y in REAL )

consider L2f being Function such that

A62: L2 = L2f and

A63: dom L2f = the carrier of V and

A64: rng L2f c= REAL by FUNCT_2:def 2;

assume y in rng fm2 ; :: thesis: y in REAL

then consider x being object such that

A65: x in dom fm2 and

A66: fm2 . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A65;

A67: fm2 . x = L2 . (Fm . x) by A45, A65;

x in Seg (len Fm) by A45, A65, FINSEQ_1:def 3;

then x in dom Fm by FINSEQ_1:def 3;

then A68: Fm . x in rng Fm by FUNCT_1:3;

rng Fm c= the carrier of V by FINSEQ_1:def 4;

then reconsider Fmx = Fm . x as Element of V by A68;

Fmx in dom L2f by A63;

then fm2 . x in rng L2f by A67, A62, FUNCT_1:3;

hence y in REAL by A66, A64; :: thesis: verum

end;consider L2f being Function such that

A62: L2 = L2f and

A63: dom L2f = the carrier of V and

A64: rng L2f c= REAL by FUNCT_2:def 2;

assume y in rng fm2 ; :: thesis: y in REAL

then consider x being object such that

A65: x in dom fm2 and

A66: fm2 . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A65;

A67: fm2 . x = L2 . (Fm . x) by A45, A65;

x in Seg (len Fm) by A45, A65, FINSEQ_1:def 3;

then x in dom Fm by FINSEQ_1:def 3;

then A68: Fm . x in rng Fm by FUNCT_1:3;

rng Fm c= the carrier of V by FINSEQ_1:def 4;

then reconsider Fmx = Fm . x as Element of V by A68;

Fmx in dom L2f by A63;

then fm2 . x in rng L2f by A67, A62, FUNCT_1:3;

hence y in REAL by A66, A64; :: thesis: verum

A69: len (r * fm1) = len fm1 by RVSUM_1:117

.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;

rng fb c= REAL

proof

then reconsider fb = fb as FinSequence of REAL by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng fb or y in REAL )

consider L2f being Function such that

A70: L2 = L2f and

A71: dom L2f = the carrier of V and

A72: rng L2f c= REAL by FUNCT_2:def 2;

assume y in rng fb ; :: thesis: y in REAL

then consider x being object such that

A73: x in dom fb and

A74: fb . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A73;

A75: fb . x = L2 . (Fb . x) by A61, A73;

x in Seg (len Fb) by A61, A73, FINSEQ_1:def 3;

then x in dom Fb by FINSEQ_1:def 3;

then A76: Fb . x in rng Fb by FUNCT_1:3;

rng Fb c= the carrier of V by FINSEQ_1:def 4;

then reconsider Fbx = Fb . x as Element of V by A76;

Fbx in dom L2f by A71;

then fb . x in rng L2f by A75, A70, FUNCT_1:3;

hence y in REAL by A74, A72; :: thesis: verum

end;consider L2f being Function such that

A70: L2 = L2f and

A71: dom L2f = the carrier of V and

A72: rng L2f c= REAL by FUNCT_2:def 2;

assume y in rng fb ; :: thesis: y in REAL

then consider x being object such that

A73: x in dom fb and

A74: fb . x = y by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A73;

A75: fb . x = L2 . (Fb . x) by A61, A73;

x in Seg (len Fb) by A61, A73, FINSEQ_1:def 3;

then x in dom Fb by FINSEQ_1:def 3;

then A76: Fb . x in rng Fb by FUNCT_1:3;

rng Fb c= the carrier of V by FINSEQ_1:def 4;

then reconsider Fbx = Fb . x as Element of V by A76;

Fbx in dom L2f by A71;

then fb . x in rng L2f by A75, A70, FUNCT_1:3;

hence y in REAL by A74, A72; :: thesis: verum

set f = ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb);

consider f1 being FinSequence of REAL such that

A77: len f1 = len F1 and

A78: Sum f1 = 1 and

A79: for n being Nat st n in dom f1 holds

( f1 . n = L1 . (F1 . n) & f1 . n >= 0 ) by A9;

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:22

.= ((len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by FINSEQ_1:22

.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len ((1 - r) * fb)) by RVSUM_1:117

.= ((len ft) + (len ((r * fm1) + ((1 - r) * fm2)))) + (len fb) by RVSUM_1:117

.= ((len ft) + (len (r * fm1))) + (len fb) by A69, INTEGRA5:2

.= ((len Ft) + (len Fm)) + (len Fb) by A29, A37, A61, RVSUM_1:117

.= (len (Ft ^ Fm)) + (len Fb) by FINSEQ_1:22 ;

then A80: len (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) = len ((Ft ^ Fm) ^ Fb) by FINSEQ_1:22;

A81: dom L1 = the carrier of V by FUNCT_2:92;

A82: for x being object holds

( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )

proof

A85:
rng (Ft ^ Fm) = (Carrier Lt) \/ (Carrier Lm)
by A18, A22, FINSEQ_1:31;
let x be object ; :: thesis: ( x in dom f1 iff ( x in dom F1 & F1 . x in dom L1 ) )

end;A83: now :: thesis: ( x in dom f1 implies ( x in dom F1 & F1 . x in dom L1 ) )

assume
x in dom f1
; :: thesis: ( x in dom F1 & F1 . x in dom L1 )

then x in Seg (len F1) by A77, FINSEQ_1:def 3;

hence x in dom F1 by FINSEQ_1:def 3; :: thesis: F1 . x in dom L1

then F1 . x in rng F1 by FUNCT_1:3;

hence F1 . x in dom L1 by A8, A81; :: thesis: verum

end;then x in Seg (len F1) by A77, FINSEQ_1:def 3;

hence x in dom F1 by FINSEQ_1:def 3; :: thesis: F1 . x in dom L1

then F1 . x in rng F1 by FUNCT_1:3;

hence F1 . x in dom L1 by A8, A81; :: thesis: verum

now :: thesis: ( x in dom F1 & F1 . x in dom L1 implies x in dom f1 )

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

A84: x in dom F1 and

F1 . x in dom L1 ; :: thesis: x in dom f1

x in Seg (len F1) by A84, FINSEQ_1:def 3;

hence x in dom f1 by A77, FINSEQ_1:def 3; :: thesis: verum

end;A84: x in dom F1 and

F1 . x in dom L1 ; :: thesis: x in dom f1

x in Seg (len F1) by A84, FINSEQ_1:def 3;

hence x in dom f1 by A77, FINSEQ_1:def 3; :: thesis: verum

for x being object st x in dom f1 holds

f1 . x = L1 . (F1 . x) by A79;

then A86: f1 = L1 * F1 by A82, FUNCT_1:10;

Ft ^ Fm is one-to-one by A17, A21, A24, FINSEQ_3:91;

then A87: F1,Ft ^ Fm are_fiberwise_equipotent by A7, A23, RFINSEQ:26;

then dom F1 = dom (Ft ^ Fm) by RFINSEQ:3;

then A88: Sum f1 = Sum (ft ^ fm1) by A8, A87, A81, A86, A85, A56, CLASSES1:83, RFINSEQ:9;

A89: rng (Fm ^ Fb) = (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;

for x being object st x in dom f2 holds

f2 . x = L2 . (F2 . x) by A28;

then A90: f2 = L2 * F2 by A58, FUNCT_1:10;

A91: rng (Fm ^ Fb) = ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier (r * L1))) \/ ((Carrier (r * L1)) /\ (Carrier ((1 - r) * L2))) by A15, A16, A22, A20, FINSEQ_1:31

.= (((Carrier L1) \/ (Carrier L2)) \ (Carrier L1)) \/ ((Carrier L1) /\ (Carrier L2)) by A13, A3, A12, Lm5

.= (((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 A5 ;

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

then A128:
for n being Nat st n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) holds
let n be Element of NAT ; :: thesis: ( n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) implies ( (((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 ) )

assume A92: n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) ; :: thesis: ( (((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 )

end;assume A92: n in dom (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) ; :: thesis: ( (((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 )

now :: thesis: ( (((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 )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: verumper cases
( n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) or ex m being Nat st

( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ) by A92, FINSEQ_1:25;

end;

( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ) by A92, FINSEQ_1:25;

suppose A93:
n in dom ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))
; :: thesis: ( (((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 )

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

end;now :: thesis: ( (((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 )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: verumper cases
( n in dom (r * ft) or ex k being Nat st

( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ) by A93, FINSEQ_1:25;

end;

( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ) by A93, FINSEQ_1:25;

suppose A95:
n in dom (r * ft)
; :: thesis: ( (((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 )

len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) =
(len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2)))
by FINSEQ_1:22

.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117

.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2

.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117

.= len (Ft ^ Fm) by FINSEQ_1:22 ;

then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def 3;

then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;

then A96: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;

A97: n in dom ft by A95, VALUED_1:def 5;

then n in Seg (len Ft) by A29, FINSEQ_1:def 3;

then A98: n in dom Ft by FINSEQ_1:def 3;

then A99: Ft . n in Carrier Lt by A18, FUNCT_1:3;

then reconsider Ftn = Ft . n as Element of V ;

A100: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = (r * ft) . n by A94, A95, FINSEQ_1:def 7

.= r * (ft . n) by RVSUM_1:44

.= r * (L1 . (Ft . n)) by A29, A97 ;

not Ft . n in Carrier L2 by A12, A10, A99, XBOOLE_0:def 5;

then L2 . Ftn = 0 by RLVECT_2:19;

then (1 - r) * (L2 . Ftn) = 0 ;

then ((1 - r) * L2) . Ftn = 0 by RLVECT_2:def 11;

then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Ftn) + (((1 - r) * L2) . Ftn) by A100, RLVECT_2:def 11

.= ((r * L1) + ((1 - r) * L2)) . (Ft . n) by RLVECT_2:def 10 ;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A98, A96, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0

A101: rng Ft c= rng (Ft ^ Fm) by FINSEQ_1:29;

Ft . n in rng Ft by A98, FUNCT_1:3;

then consider m9 being object such that

A102: m9 in dom F1 and

A103: F1 . m9 = Ft . n by A23, A101, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A102;

m9 in Seg (len f1) by A77, A102, FINSEQ_1:def 3;

then m9 in dom f1 by FINSEQ_1:def 3;

then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A1, A100, A103; :: thesis: verum

end;.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117

.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2

.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117

.= len (Ft ^ Fm) by FINSEQ_1:22 ;

then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def 3;

then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;

then A96: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;

A97: n in dom ft by A95, VALUED_1:def 5;

then n in Seg (len Ft) by A29, FINSEQ_1:def 3;

then A98: n in dom Ft by FINSEQ_1:def 3;

then A99: Ft . n in Carrier Lt by A18, FUNCT_1:3;

then reconsider Ftn = Ft . n as Element of V ;

A100: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = (r * ft) . n by A94, A95, FINSEQ_1:def 7

.= r * (ft . n) by RVSUM_1:44

.= r * (L1 . (Ft . n)) by A29, A97 ;

not Ft . n in Carrier L2 by A12, A10, A99, XBOOLE_0:def 5;

then L2 . Ftn = 0 by RLVECT_2:19;

then (1 - r) * (L2 . Ftn) = 0 ;

then ((1 - r) * L2) . Ftn = 0 by RLVECT_2:def 11;

then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Ftn) + (((1 - r) * L2) . Ftn) by A100, RLVECT_2:def 11

.= ((r * L1) + ((1 - r) * L2)) . (Ft . n) by RLVECT_2:def 10 ;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A98, A96, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0

A101: rng Ft c= rng (Ft ^ Fm) by FINSEQ_1:29;

Ft . n in rng Ft by A98, FUNCT_1:3;

then consider m9 being object such that

A102: m9 in dom F1 and

A103: F1 . m9 = Ft . n by A23, A101, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A102;

m9 in Seg (len f1) by A77, A102, FINSEQ_1:def 3;

then m9 in dom f1 by FINSEQ_1:def 3;

then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A1, A100, A103; :: thesis: verum

suppose
ex k being Nat st

( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ; :: thesis: ( (((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 )

( k in dom ((r * fm1) + ((1 - r) * fm2)) & n = (len (r * ft)) + k ) ; :: thesis: ( (((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 )

then consider m being Element of NAT such that

A104: m in dom ((r * fm1) + ((1 - r) * fm2)) and

A105: n = (len (r * ft)) + m ;

len (r * fm1) = len fm1 by RVSUM_1:117

.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;

then A106: len ((r * fm1) + ((1 - r) * fm2)) = len (r * fm1) by INTEGRA5:2

.= len fm1 by RVSUM_1:117 ;

then A107: m in dom Fm by A37, A104, FINSEQ_3:29;

then A108: Fm . m in rng Fm by FUNCT_1:3;

then reconsider Fmm = Fm . m as Element of V by A22;

A109: m in dom fm1 by A104, A106, FINSEQ_3:29;

A110: m in dom fm2 by A37, A45, A104, A106, FINSEQ_3:29;

A111: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * fm1) + ((1 - r) * fm2)) . m by A94, A104, A105, FINSEQ_1:def 7

.= ((r * fm1) . m) + (((1 - r) * fm2) . m) by A104, VALUED_1:def 1

.= (r * (fm1 . m)) + (((1 - r) * fm2) . m) by RVSUM_1:44

.= (r * (fm1 . m)) + ((1 - r) * (fm2 . m)) by RVSUM_1:44

.= (r * (L1 . (Fm . m))) + ((1 - r) * (fm2 . m)) by A37, A109

.= (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) by A45, A110 ;

len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22

.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117

.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2

.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117

.= len (Ft ^ Fm) by FINSEQ_1:22 ;

then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def 3;

then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;

then A112: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;

A113: len (r * ft) = len Ft by A29, RVSUM_1:117;

( r * (L1 . Fmm) = (r * L1) . (Fm . m) & (1 - r) * (L2 . Fmm) = ((1 - r) * L2) . (Fm . m) ) by RLVECT_2:def 11;

then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (Fm . m) by A111, RLVECT_2:def 10;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A105, A107, A112, A113, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0

rng Fm c= rng (Ft ^ Fm) by FINSEQ_1:30;

then consider m9 being object such that

A114: m9 in dom F1 and

A115: F1 . m9 = Fm . m by A23, A108, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A114;

m9 in Seg (len F1) by A114, FINSEQ_1:def 3;

then m9 in dom f1 by A77, FINSEQ_1:def 3;

then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;

then A116: r * (L1 . (Fm . m)) >= 0 by A1, A115;

rng Fm c= rng (Fm ^ Fb) by FINSEQ_1:29;

then consider m9 being object such that

A117: m9 in dom F2 and

A118: F2 . m9 = Fm . m by A91, A108, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A117;

m9 in Seg (len F2) by A117, FINSEQ_1:def 3;

then m9 in dom f2 by A26, FINSEQ_1:def 3;

then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;

then (1 - r) * (L2 . (Fm . m)) >= 0 by A11, A118;

then (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) >= 0 + 0 by A116;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A111; :: thesis: verum

end;A104: m in dom ((r * fm1) + ((1 - r) * fm2)) and

A105: n = (len (r * ft)) + m ;

len (r * fm1) = len fm1 by RVSUM_1:117

.= len ((1 - r) * fm2) by A37, A45, RVSUM_1:117 ;

then A106: len ((r * fm1) + ((1 - r) * fm2)) = len (r * fm1) by INTEGRA5:2

.= len fm1 by RVSUM_1:117 ;

then A107: m in dom Fm by A37, A104, FINSEQ_3:29;

then A108: Fm . m in rng Fm by FUNCT_1:3;

then reconsider Fmm = Fm . m as Element of V by A22;

A109: m in dom fm1 by A104, A106, FINSEQ_3:29;

A110: m in dom fm2 by A37, A45, A104, A106, FINSEQ_3:29;

A111: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * fm1) + ((1 - r) * fm2)) . m by A94, A104, A105, FINSEQ_1:def 7

.= ((r * fm1) . m) + (((1 - r) * fm2) . m) by A104, VALUED_1:def 1

.= (r * (fm1 . m)) + (((1 - r) * fm2) . m) by RVSUM_1:44

.= (r * (fm1 . m)) + ((1 - r) * (fm2 . m)) by RVSUM_1:44

.= (r * (L1 . (Fm . m))) + ((1 - r) * (fm2 . m)) by A37, A109

.= (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) by A45, A110 ;

len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22

.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117

.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2

.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117

.= len (Ft ^ Fm) by FINSEQ_1:22 ;

then n in Seg (len (Ft ^ Fm)) by A93, FINSEQ_1:def 3;

then n in dom (Ft ^ Fm) by FINSEQ_1:def 3;

then A112: (Ft ^ Fm) . n = ((Ft ^ Fm) ^ Fb) . n by FINSEQ_1:def 7;

A113: len (r * ft) = len Ft by A29, RVSUM_1:117;

( r * (L1 . Fmm) = (r * L1) . (Fm . m) & (1 - r) * (L2 . Fmm) = ((1 - r) * L2) . (Fm . m) ) by RLVECT_2:def 11;

then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (Fm . m) by A111, RLVECT_2:def 10;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A105, A107, A112, A113, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0

rng Fm c= rng (Ft ^ Fm) by FINSEQ_1:30;

then consider m9 being object such that

A114: m9 in dom F1 and

A115: F1 . m9 = Fm . m by A23, A108, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A114;

m9 in Seg (len F1) by A114, FINSEQ_1:def 3;

then m9 in dom f1 by A77, FINSEQ_1:def 3;

then ( f1 . m9 = L1 . (F1 . m9) & f1 . m9 >= 0 ) by A79;

then A116: r * (L1 . (Fm . m)) >= 0 by A1, A115;

rng Fm c= rng (Fm ^ Fb) by FINSEQ_1:29;

then consider m9 being object such that

A117: m9 in dom F2 and

A118: F2 . m9 = Fm . m by A91, A108, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A117;

m9 in Seg (len F2) by A117, FINSEQ_1:def 3;

then m9 in dom f2 by A26, FINSEQ_1:def 3;

then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;

then (1 - r) * (L2 . (Fm . m)) >= 0 by A11, A118;

then (r * (L1 . (Fm . m))) + ((1 - r) * (L2 . (Fm . m))) >= 0 + 0 by A116;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A111; :: thesis: verum

suppose
ex m being Nat st

( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ; :: thesis: ( (((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 )

( m in dom ((1 - r) * fb) & n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ) ; :: thesis: ( (((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 )

then consider m being Element of NAT such that

A119: m in dom ((1 - r) * fb) and

A120: n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ;

A121: m in dom fb by A119, VALUED_1:def 5;

then m in Seg (len Fb) by A61, FINSEQ_1:def 3;

then A122: m in dom Fb by FINSEQ_1:def 3;

then A123: Fb . m in rng Fb by FUNCT_1:3;

then reconsider Fbm = Fb . m as Element of V by A20;

A124: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((1 - r) * fb) . m by A119, A120, FINSEQ_1:def 7

.= (1 - r) * (fb . m) by RVSUM_1:44

.= (1 - r) * (L2 . (Fb . m)) by A61, A121 ;

A125: len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22

.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117

.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2

.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117

.= len (Ft ^ Fm) by FINSEQ_1:22 ;

not Fb . m in Carrier L1 by A3, A16, A20, A123, XBOOLE_0:def 5;

then L1 . Fbm = 0 by RLVECT_2:19;

then r * (L1 . Fbm) = 0 ;

then (r * L1) . Fbm = 0 by RLVECT_2:def 11;

then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Fbm) + (((1 - r) * L2) . Fbm) by A124, RLVECT_2:def 11

.= ((r * L1) + ((1 - r) * L2)) . (Fb . m) by RLVECT_2:def 10 ;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A120, A122, A125, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0

rng Fb c= rng (Fm ^ Fb) by FINSEQ_1:30;

then consider m9 being object such that

A126: m9 in dom F2 and

A127: F2 . m9 = Fb . m by A91, A123, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A126;

m9 in Seg (len F2) by A126, FINSEQ_1:def 3;

then m9 in dom f2 by A26, FINSEQ_1:def 3;

then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A11, A124, A127; :: thesis: verum

end;A119: m in dom ((1 - r) * fb) and

A120: n = (len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2)))) + m ;

A121: m in dom fb by A119, VALUED_1:def 5;

then m in Seg (len Fb) by A61, FINSEQ_1:def 3;

then A122: m in dom Fb by FINSEQ_1:def 3;

then A123: Fb . m in rng Fb by FUNCT_1:3;

then reconsider Fbm = Fb . m as Element of V by A20;

A124: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((1 - r) * fb) . m by A119, A120, FINSEQ_1:def 7

.= (1 - r) * (fb . m) by RVSUM_1:44

.= (1 - r) * (L2 . (Fb . m)) by A61, A121 ;

A125: len ((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) = (len (r * ft)) + (len ((r * fm1) + ((1 - r) * fm2))) by FINSEQ_1:22

.= (len ft) + (len ((r * fm1) + ((1 - r) * fm2))) by RVSUM_1:117

.= (len ft) + (len (r * fm1)) by A69, INTEGRA5:2

.= (len Ft) + (len Fm) by A29, A37, RVSUM_1:117

.= len (Ft ^ Fm) by FINSEQ_1:22 ;

not Fb . m in Carrier L1 by A3, A16, A20, A123, XBOOLE_0:def 5;

then L1 . Fbm = 0 by RLVECT_2:19;

then r * (L1 . Fbm) = 0 ;

then (r * L1) . Fbm = 0 by RLVECT_2:def 11;

then (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) . Fbm) + (((1 - r) * L2) . Fbm) by A124, RLVECT_2:def 11

.= ((r * L1) + ((1 - r) * L2)) . (Fb . m) by RLVECT_2:def 10 ;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n = ((r * L1) + ((1 - r) * L2)) . (((Ft ^ Fm) ^ Fb) . n) by A120, A122, A125, FINSEQ_1:def 7; :: thesis: (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0

rng Fb c= rng (Fm ^ Fb) by FINSEQ_1:30;

then consider m9 being object such that

A126: m9 in dom F2 and

A127: F2 . m9 = Fb . m by A91, A123, FUNCT_1:def 3;

reconsider m9 = m9 as Element of NAT by A126;

m9 in Seg (len F2) by A126, FINSEQ_1:def 3;

then m9 in dom f2 by A26, FINSEQ_1:def 3;

then ( f2 . m9 = L2 . (F2 . m9) & f2 . m9 >= 0 ) by A28;

hence (((r * ft) ^ ((r * fm1) + ((1 - r) * fm2))) ^ ((1 - r) * fb)) . n >= 0 by A11, A124, A127; :: thesis: verum

( (((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 ) ;

A129: rng Fb = (Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1) by A1, A16, A20, RLVECT_2:42;

then rng (Ft ^ Fm) misses rng Fb by A8, A23, XBOOLE_1:79;

then A130: (Ft ^ Fm) ^ Fb is one-to-one by A19, A25, FINSEQ_3:91;

A131: for x being object st x in dom (fm2 ^ fb) holds

(fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

proof

for x being object holds
let x be object ; :: thesis: ( x in dom (fm2 ^ fb) implies (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) )

assume A132: x in dom (fm2 ^ fb) ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

then reconsider n = x as Element of NAT ;

end;assume A132: x in dom (fm2 ^ fb) ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

then reconsider n = x as Element of NAT ;

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

hence
(fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)
; :: thesis: verumper cases
( n in dom fm2 or ex m being Nat st

( m in dom fb & n = (len fm2) + m ) ) by A132, FINSEQ_1:25;

end;

( m in dom fb & n = (len fm2) + m ) ) by A132, FINSEQ_1:25;

suppose A133:
n in dom fm2
; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

then
n in Seg (len Fm)
by A45, FINSEQ_1:def 3;

then A134: n in dom Fm by FINSEQ_1:def 3;

fm2 . n = L2 . (Fm . n) by A45, A133;

then (fm2 ^ fb) . n = L2 . (Fm . n) by A133, FINSEQ_1:def 7;

hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A134, FINSEQ_1:def 7; :: thesis: verum

end;then A134: n in dom Fm by FINSEQ_1:def 3;

fm2 . n = L2 . (Fm . n) by A45, A133;

then (fm2 ^ fb) . n = L2 . (Fm . n) by A133, FINSEQ_1:def 7;

hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A134, FINSEQ_1:def 7; :: thesis: verum

suppose
ex m being Nat st

( m in dom fb & n = (len fm2) + m ) ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

( m in dom fb & n = (len fm2) + m ) ; :: thesis: (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x)

then consider m being Element of NAT such that

A135: m in dom fb and

A136: n = (len fm2) + m ;

m in Seg (len Fb) by A61, A135, FINSEQ_1:def 3;

then A137: m in dom Fb by FINSEQ_1:def 3;

(fm2 ^ fb) . n = fb . m by A135, A136, FINSEQ_1:def 7

.= L2 . (Fb . m) by A61, A135 ;

hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A45, A136, A137, FINSEQ_1:def 7; :: thesis: verum

end;A135: m in dom fb and

A136: n = (len fm2) + m ;

m in Seg (len Fb) by A61, A135, FINSEQ_1:def 3;

then A137: m in dom Fb by FINSEQ_1:def 3;

(fm2 ^ fb) . n = fb . m by A135, A136, FINSEQ_1:def 7

.= L2 . (Fb . m) by A61, A135 ;

hence (fm2 ^ fb) . x = L2 . ((Fm ^ Fb) . x) by A45, A136, A137, FINSEQ_1:def 7; :: thesis: verum

( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )

proof

then A141:
fm2 ^ fb = L2 * (Fm ^ Fb)
by A131, FUNCT_1:10;
let x be object ; :: thesis: ( x in dom (fm2 ^ fb) iff ( x in dom (Fm ^ Fb) & (Fm ^ Fb) . x in dom L2 ) )

A138: len (fm2 ^ fb) = (len fm2) + (len fb) by FINSEQ_1:22

.= len (Fm ^ Fb) by A45, A61, FINSEQ_1:22 ;

A139: dom (fm2 ^ fb) = Seg (len (fm2 ^ fb)) by FINSEQ_1:def 3

.= dom (Fm ^ Fb) by A138, FINSEQ_1:def 3 ;

( x in dom (fm2 ^ fb) implies (Fm ^ Fb) . x in dom L2 )

end;A138: len (fm2 ^ fb) = (len fm2) + (len fb) by FINSEQ_1:22

.= len (Fm ^ Fb) by A45, A61, FINSEQ_1:22 ;

A139: dom (fm2 ^ fb) = Seg (len (fm2 ^ fb)) by FINSEQ_1:def 3

.= dom (Fm ^ Fb) by A138, FINSEQ_1:def 3 ;

( x in dom (fm2 ^ fb) implies (Fm ^ Fb) . x in dom L2 )

proof

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

then (Fm ^ Fb) . x in rng (Fm ^ Fb) by A139, FUNCT_1:3;

then A140: (Fm ^ Fb) . x in (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;

dom L2 = the carrier of V by FUNCT_2:92;

hence (Fm ^ Fb) . x in dom L2 by A140; :: thesis: verum

end;then (Fm ^ Fb) . x in rng (Fm ^ Fb) by A139, FUNCT_1:3;

then A140: (Fm ^ Fb) . x in (Carrier Lm) \/ (Carrier Lb) by A22, A20, FINSEQ_1:31;

dom L2 = the carrier of V by FUNCT_2:92;

hence (Fm ^ Fb) . x in dom L2 by A140; :: thesis: verum

rng Fm misses rng Fb by A15, A16, A22, A20, XBOOLE_1:17, XBOOLE_1:85;

then Fm ^ Fb is one-to-one by A21, A19, FINSEQ_3:91;

then A142: F2,Fm ^ Fb are_fiberwise_equipotent by A4, A91, RFINSEQ:26;

then dom F2 = dom (Fm ^ Fb) by RFINSEQ:3;

then A143: Sum f2 = Sum (fm2 ^ fb) by A5, A142, A57, A90, A89, A141, CLASSES1:83, RFINSEQ:9;

A144: 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:75

.= ((Sum (r * ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:75

.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + (Sum ((1 - r) * fb)) by RVSUM_1:87

.= ((r * (Sum ft)) + (Sum ((r * fm1) + ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87

.= ((r * (Sum ft)) + ((Sum (r * fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by A69, INTEGRA5:2

.= ((r * (Sum ft)) + ((r * (Sum fm1)) + (Sum ((1 - r) * fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87

.= ((r * (Sum ft)) + ((r * (Sum fm1)) + ((1 - r) * (Sum fm2)))) + ((1 - r) * (Sum fb)) by RVSUM_1:87

.= (r * ((Sum ft) + (Sum fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb)))

.= (r * (Sum (ft ^ fm1))) + ((1 - r) * ((Sum fm2) + (Sum fb))) by RVSUM_1:75

.= (r * 1) + ((1 - r) * 1) by A78, A27, A88, A143, RVSUM_1:75

.= 0 + 1 ;

rng ((Ft ^ Fm) ^ Fb) = (Carrier L1) \/ ((Carrier ((r * L1) + ((1 - r) * L2))) \ (Carrier L1)) by A8, A23, A129, FINSEQ_1:31

.= (Carrier L1) \/ (Carrier ((r * L1) + ((1 - r) * L2))) by XBOOLE_1:39

.= Carrier ((r * L1) + ((1 - r) * L2)) by A3, A14, XBOOLE_1:7, XBOOLE_1:12 ;

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