let X be set ; :: thesis: for S being with_empty_element cap-closed Subset-Family of X
for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed nonnegative Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )
let S be with_empty_element cap-closed Subset-Family of X; :: thesis: for F1, F2 being non empty disjoint_valued FinSequence of S
for P being zeroed nonnegative Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )
let F1, F2 be non empty disjoint_valued FinSequence of S; :: thesis: for P being zeroed nonnegative Function of S,ExtREAL
for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )
let P be zeroed nonnegative Function of S,ExtREAL; :: thesis: for Mx being Matrix of len F1, len F2,ExtREAL st Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) holds
( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )
let Mx be Matrix of len F1, len F2,ExtREAL; :: thesis: ( Union F1 = Union F2 & ( for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) ) & ( for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ) implies ( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) ) )
assume that
A1: Union F1 = Union F2 and
A2: for i, j being Nat st [i,j] in Indices Mx holds
Mx * (i,j) = P . ((F1 . i) /\ (F2 . j)) and
A3: for F being disjoint_valued FinSequence of S st Union F in S holds
P . (Union F) = Sum (P * F) ; :: thesis: ( ( for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i ) & Sum (P * F2) = SumAll (Mx @) )
consider Kx being Matrix of len F1, len F2,S such that
KX1: for i, j being Nat st [i,j] in Indices Kx holds
Kx * (i,j) = (F1 . i) /\ (F2 . j) by FStoMAT1;
A5: len (P * F2) = len F2 by FINSEQ_2:33;
C3: ( len Kx = len F1 & len Mx = len F1 ) by MATRIX_0:def 2;
then ( width Kx = len F2 & width Mx = len F2 ) by MATRIX_0:20;
then C5: ( len (Kx @) = len F2 & len (Mx @) = len F2 & width (Kx @) = len F1 & width (Mx @) = len F1 ) by C3, MATRIX_0:29;
then D2: len (P * F2) = len (Sum (Mx @)) by A5, Def5;
thus D6: for i being Nat st i <= len (P * F2) holds
(P * F2) . i = (Sum (Mx @)) . i :: thesis: Sum (P * F2) = SumAll (Mx @)

proof

let i be Nat; :: thesis: ( i <= len (P * F2) implies (P * F2) . i = (Sum (Mx @)) . i )
assume E0: i <= len (P * F2) ; :: thesis: (P * F2) . i = (Sum (Mx @)) . i

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: (P * F2) . i = (Sum (Mx @)) . i

then ( not i in dom (P * F2) & not i in dom (Sum (Mx @)) ) by FINSEQ_3:24;
then ( (P * F2) . i = 0 & (Sum (Mx @)) . i = 0 ) by FUNCT_1:def 2;
hence (P * F2) . i = (Sum (Mx @)) . i ; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: (P * F2) . i = (Sum (Mx @)) . i

then E1: 1 <= i by NAT_1:14;
then i in dom (P * F2) by E0, FINSEQ_3:25;
then E2: i in dom F2 by FUNCT_1:11;
then F2 . i c= union (rng F2) by FUNCT_1:3, ZFMISC_1:74;
then F2 . i c= Union F1 by A1, CARD_3:def 4;
then E3: (F2 . i) /\ (Union F1) = F2 . i by XBOOLE_1:28;
E4: F2 . i in rng F2 by E2, FUNCT_1:3;
E5: ( i in dom (Kx @) & i in dom (Mx @) ) by C5, A5, E0, E1, FINSEQ_3:25;
for p, q being object st p <> q holds
((Kx @) . i) . p misses ((Kx @) . i) . q

proof

let p, q be object ; :: thesis: ( p <> q implies ((Kx @) . i) . p misses ((Kx @) . i) . q )
assume SA0: p <> q ; :: thesis: ((Kx @) . i) . p misses ((Kx @) . i) . q

per cases ( ( p in dom ((Kx @) . i) & q in dom ((Kx @) . i) ) or not p in dom ((Kx @) . i) or not q in dom ((Kx @) . i) ) ;

suppose SA1: ( p in dom ((Kx @) . i) & q in dom ((Kx @) . i) ) ; :: thesis: ((Kx @) . i) . p misses ((Kx @) . i) . q

then reconsider p1 = p, q1 = q as Nat ;
E6: ( [i,p1] in Indices (Kx @) & [i,q1] in Indices (Kx @) ) by SA1, E5, MATRIX_0:37;
then EE6: ( [p1,i] in Indices Kx & [q1,i] in Indices Kx ) by MATRIX_0:def 6;
( (Kx @) * (i,p1) = ((Kx @) . i) . p & (Kx @) * (i,q1) = ((Kx @) . i) . q ) by E6, MATRPROB:14;
then ( ((Kx @) . i) . p = Kx * (p1,i) & ((Kx @) . i) . q = Kx * (q1,i) ) by EE6, MATRIX_0:def 6;
then ( ((Kx @) . i) . p = (F2 . i) /\ (F1 . p1) & ((Kx @) . i) . q = (F2 . i) /\ (F1 . q1) ) by EE6, KX1;
hence ((Kx @) . i) . p misses ((Kx @) . i) . q by SA0, PROB_2:def 2, XBOOLE_1:76; :: thesis: verum

end;

suppose not p in dom ((Kx @) . i) ; :: thesis: ((Kx @) . i) . p misses ((Kx @) . i) . q

then ((Kx @) . i) . p = {} by FUNCT_1:def 2;
hence ((Kx @) . i) . p misses ((Kx @) . i) . q by XBOOLE_1:65; :: thesis: verum

end;

suppose not q in dom ((Kx @) . i) ; :: thesis: ((Kx @) . i) . p misses ((Kx @) . i) . q

then ((Kx @) . i) . q = {} by FUNCT_1:def 2;
hence ((Kx @) . i) . p misses ((Kx @) . i) . q by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

then E8: (Kx @) . i is disjoint_valued FinSequence of S by PROB_2:def 2;

now :: thesis: for x being object st x in Union ((Kx @) . i) holds
x in (F2 . i) /\ (Union F1)

let x be object ; :: thesis: ( x in Union ((Kx @) . i) implies x in (F2 . i) /\ (Union F1) )
assume x in Union ((Kx @) . i) ; :: thesis: x in (F2 . i) /\ (Union F1)
then x in union (rng ((Kx @) . i)) by CARD_3:def 4;
then consider A being set such that
E9: ( x in A & A in rng ((Kx @) . i) ) by TARSKI:def 4;
consider m being object such that
E10: ( m in dom ((Kx @) . i) & A = ((Kx @) . i) . m ) by E9, FUNCT_1:def 3;
reconsider m = m as Nat by E10;
E11: [i,m] in Indices (Kx @) by E10, E5, MATRIX_0:37;
then EE11: [m,i] in Indices Kx by MATRIX_0:def 6;
((Kx @) . i) . m = (Kx @) * (i,m) by E11, MATRPROB:14;
then ((Kx @) . i) . m = Kx * (m,i) by EE11, MATRIX_0:def 6;
then ((Kx @) . i) . m = (F2 . i) /\ (F1 . m) by EE11, KX1;
then E12: ( x in F2 . i & x in F1 . m ) by E9, E10, XBOOLE_0:def 4;
( 1 <= m & m <= len F1 ) by EE11, MATRIX_0:33;
then m in dom F1 by FINSEQ_3:25;
then F1 . m in rng F1 by FUNCT_1:3;
then x in union (rng F1) by E12, TARSKI:def 4;
then x in Union F1 by CARD_3:def 4;
hence x in (F2 . i) /\ (Union F1) by E12, XBOOLE_0:def 4; :: thesis: verum

end;

then E13: Union ((Kx @) . i) c= (F2 . i) /\ (Union F1) by TARSKI:def 3;

now :: thesis: for x being object st x in (F2 . i) /\ (Union F1) holds
x in Union ((Kx @) . i)

let x be object ; :: thesis: ( x in (F2 . i) /\ (Union F1) implies x in Union ((Kx @) . i) )
assume x in (F2 . i) /\ (Union F1) ; :: thesis: x in Union ((Kx @) . i)
then E14: ( x in F2 . i & x in Union F1 ) by XBOOLE_0:def 4;
then x in union (rng F1) by CARD_3:def 4;
then consider A being set such that
E15: ( x in A & A in rng F1 ) by TARSKI:def 4;
consider m being object such that
E16: ( m in dom F1 & A = F1 . m ) by E15, FUNCT_1:def 3;
reconsider m = m as Nat by E16;
( 1 <= i & i <= len F2 & 1 <= m & m <= len F1 ) by E2, E16, FINSEQ_3:25;
then EE17: [m,i] in Indices Kx by MATRIX_0:31;
then E17: [i,m] in Indices (Kx @) by MATRIX_0:def 6;
((Kx @) . i) . m = (Kx @) * (i,m) by E17, MATRPROB:14;
then ((Kx @) . i) . m = Kx * (m,i) by EE17, MATRIX_0:def 6;
then ((Kx @) . i) . m = (F2 . i) /\ (F1 . m) by EE17, KX1;
then E18: x in ((Kx @) . i) . m by E14, E15, E16, XBOOLE_0:def 4;
m in dom ((Kx @) . i) by E17, MATRIX_0:38;
then ((Kx @) . i) . m in rng ((Kx @) . i) by FUNCT_1:3;
then x in union (rng ((Kx @) . i)) by E18, TARSKI:def 4;
hence x in Union ((Kx @) . i) by CARD_3:def 4; :: thesis: verum

end;

then (F2 . i) /\ (Union F1) c= Union ((Kx @) . i) by TARSKI:def 3;
then (F2 . i) /\ (Union F1) = Union ((Kx @) . i) by E13, XBOOLE_0:def 10;
then E19: P . ((F2 . i) /\ (Union F1)) = Sum (P * ((Kx @) . i)) by E3, E4, E8, A3;
E20: i in Seg (len (Mx @)) by C5, A5, E0, E1;
E21: ( (Mx @) . i = Line ((Mx @),i) & (Kx @) . i = Line ((Kx @),i) ) by E5, MATRIX_0:60;
rng ((Kx @) . i) c= S ;
then rng ((Kx @) . i) c= dom P by FUNCT_2:def 1;
then E22: dom (P * ((Kx @) . i)) = dom ((Kx @) . i) by RELAT_1:27;
then len (P * ((Kx @) . i)) = len ((Kx @) . i) by FINSEQ_3:29;
then F23: len (P * ((Kx @) . i)) = width (Kx @) by E21, MATRIX_0:def 7;
then E23: len (P * ((Kx @) . i)) = len ((Mx @) . i) by C5, E21, MATRIX_0:def 7;
for k being Nat st 1 <= k & k <= len (P * ((Kx @) . i)) holds
(P * ((Kx @) . i)) . k = ((Mx @) . i) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (P * ((Kx @) . i)) implies (P * ((Kx @) . i)) . k = ((Mx @) . i) . k )
assume E24: ( 1 <= k & k <= len (P * ((Kx @) . i)) ) ; :: thesis: (P * ((Kx @) . i)) . k = ((Mx @) . i) . k
then ( k in dom ((Kx @) . i) & k in dom ((Mx @) . i) ) by E23, E22, FINSEQ_3:25;
then E25: ( [i,k] in Indices (Kx @) & [i,k] in Indices (Mx @) ) by E5, MATRPROB:13;
then EE25: ( [k,i] in Indices Kx & [k,i] in Indices Mx ) by MATRIX_0:def 6;
k in dom (P * ((Kx @) . i)) by E24, FINSEQ_3:25;
then (P * ((Kx @) . i)) . k = P . (((Kx @) . i) . k) by FUNCT_1:12;
then (P * ((Kx @) . i)) . k = P . ((Kx @) * (i,k)) by E25, MATRPROB:14;
then (P * ((Kx @) . i)) . k = P . (Kx * (k,i)) by EE25, MATRIX_0:def 6;
then (P * ((Kx @) . i)) . k = P . ((F2 . i) /\ (F1 . k)) by EE25, KX1;
then (P * ((Kx @) . i)) . k = Mx * (k,i) by EE25, A2;
then (P * ((Kx @) . i)) . k = (Mx @) * (i,k) by EE25, MATRIX_0:def 6;
hence (P * ((Kx @) . i)) . k = ((Mx @) . i) . k by E25, MATRPROB:14; :: thesis: verum

end;

then E27: P * ((Kx @) . i) = (Mx @) . i by F23, C5, E21, MATRIX_0:def 7;
F2 . i c= union (rng F2) by E2, FUNCT_1:3, ZFMISC_1:74;
then F2 . i c= Union F2 by CARD_3:def 4;
then (F2 . i) /\ (Union F1) = F2 . i by A1, XBOOLE_1:28;
then (P * F2) . i = Sum (P * ((Kx @) . i)) by E2, E19, FUNCT_1:13;
hence (P * F2) . i = (Sum (Mx @)) . i by E20, E27, E21, Th16; :: thesis: verum

end;

end;

end;

consider SMF2 being Function of NAT,ExtREAL such that
A3: ( Sum (P * F2) = SMF2 . (len (P * F2)) & SMF2 . 0 = 0 & ( for i being Nat st i < len (P * F2) holds
SMF2 . (i + 1) = (SMF2 . i) + ((P * F2) . (i + 1)) ) ) by EXTREAL1:def 2;
consider LL being Function of NAT,ExtREAL such that
D7: ( SumAll (Mx @) = LL . (len (Sum (Mx @))) & LL . 0 = 0. & ( for i being Nat st i < len (Sum (Mx @)) holds
LL . (i + 1) = (LL . i) + ((Sum (Mx @)) . (i + 1)) ) ) by EXTREAL1:def 2;
defpred S₁[ Nat] means ( $1 <= len (P * F2) implies SMF2 . $1 = LL . $1 );
D8: S₁[ 0 ] by A3, D7;
D9: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume V1: S₁[i] ; :: thesis: S₁[i + 1]
assume V3: i + 1 <= len (P * F2) ; :: thesis: SMF2 . (i + 1) = LL . (i + 1)
then SMF2 . (i + 1) = (SMF2 . i) + ((P * F2) . (i + 1)) by A3, NAT_1:13;
then SMF2 . (i + 1) = (LL . i) + ((Sum (Mx @)) . (i + 1)) by D6, V1, V3, NAT_1:13;
hence SMF2 . (i + 1) = LL . (i + 1) by D7, V3, D2, NAT_1:13; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(D8, D9);
hence Sum (P * F2) = SumAll (Mx @) by A3, D2, D7; :: thesis: verum