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 * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = 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 * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = 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 * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = 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 * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = 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 * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = 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 * F1) holds
(P * F1) . i = (Sum Mx) . i ) & Sum (P * F1) = 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;
C0: ( len Kx = len F1 & len Mx = len F1 ) by MATRIX_0:def 2;
then C1: ( len (P * F1) = len Mx & len (P * F1) = len Kx ) by FINSEQ_2:33;
C4: ( width Kx = len F2 & width Mx = len F2 ) by C0, MATRIX_0:20;
C2: len (P * F1) = len (Sum Mx) by C1, Def5;
thus C6: for i being Nat st i <= len (P * F1) holds
(P * F1) . i = (Sum Mx) . i :: thesis: Sum (P * F1) = SumAll Mx

proof

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

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

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

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

end;

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

then E1: 1 <= i by NAT_1:14;
then i in dom (P * F1) by E0, FINSEQ_3:25;
then E2: i in dom F1 by FUNCT_1:11;
then F1 . i c= union (rng F1) by FUNCT_1:3, ZFMISC_1:74;
then F1 . i c= Union F2 by A1, CARD_3:def 4;
then E3: (F1 . i) /\ (Union F2) = F1 . i by XBOOLE_1:28;
E4: F1 . i in rng F1 by E2, FUNCT_1:3;
E5: ( i in dom Kx & i in dom Mx ) by C1, 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;
( Kx * (i,p1) = (Kx . i) . p & Kx * (i,q1) = (Kx . i) . q ) by E6, MATRPROB:14;
then ( (Kx . i) . p = (F1 . i) /\ (F2 . p1) & (Kx . i) . q = (F1 . i) /\ (F2 . q1) ) by E6, 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 (F1 . i) /\ (Union F2)

let x be object ; :: thesis: ( x in Union (Kx . i) implies x in (F1 . i) /\ (Union F2) )
assume x in Union (Kx . i) ; :: thesis: x in (F1 . i) /\ (Union F2)
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 (Kx . i) . m = Kx * (i,m) by MATRPROB:14;
then (Kx . i) . m = (F1 . i) /\ (F2 . m) by E11, KX1;
then E12: ( x in F1 . i & x in F2 . m ) by E9, E10, XBOOLE_0:def 4;
( 1 <= m & m <= len F2 ) by E11, MATRIX_0:33;
then m in dom F2 by FINSEQ_3:25;
then F2 . m in rng F2 by FUNCT_1:3;
then x in union (rng F2) by E12, TARSKI:def 4;
then x in Union F2 by CARD_3:def 4;
hence x in (F1 . i) /\ (Union F2) by E12, XBOOLE_0:def 4; :: thesis: verum

end;

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

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

let x be object ; :: thesis: ( x in (F1 . i) /\ (Union F2) implies x in Union (Kx . i) )
assume x in (F1 . i) /\ (Union F2) ; :: thesis: x in Union (Kx . i)
then E14: ( x in F1 . i & x in Union F2 ) by XBOOLE_0:def 4;
then x in union (rng F2) by CARD_3:def 4;
then consider A being set such that
E15: ( x in A & A in rng F2 ) by TARSKI:def 4;
consider m being object such that
E16: ( m in dom F2 & A = F2 . m ) by E15, FUNCT_1:def 3;
reconsider m = m as Nat by E16;
( 1 <= i & i <= len F1 & 1 <= m & m <= len F2 ) by E2, E16, FINSEQ_3:25;
then E17: [i,m] in Indices Kx by MATRIX_0:31;
then (Kx . i) . m = Kx * (i,m) by MATRPROB:14;
then (Kx . i) . m = (F1 . i) /\ (F2 . m) by E17, 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 (F1 . i) /\ (Union F2) c= Union (Kx . i) by TARSKI:def 3;
then (F1 . i) /\ (Union F2) = Union (Kx . i) by E13, XBOOLE_0:def 10;
then E19: P . ((F1 . i) /\ (Union F2)) = Sum (P * (Kx . i)) by E3, E4, E8, A3;
E20: i in Seg (len Mx) by C1, 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 E23a: len (P * (Kx . i)) = width Kx by E21, MATRIX_0:def 7;
then E23: len (P * (Kx . i)) = len (Mx . i) by C4, 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;
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 . ((F1 . i) /\ (F2 . k)) by E25, KX1;
then (P * (Kx . i)) . k = Mx * (i,k) by E25, A2;
hence (P * (Kx . i)) . k = (Mx . i) . k by E25, MATRPROB:14; :: thesis: verum

end;

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

end;

end;

end;

consider SMF1 being Function of NAT,ExtREAL such that
A2: ( Sum (P * F1) = SMF1 . (len (P * F1)) & SMF1 . 0 = 0 & ( for i being Nat st i < len (P * F1) holds
SMF1 . (i + 1) = (SMF1 . i) + ((P * F1) . (i + 1)) ) ) by EXTREAL1:def 2;
consider LL being Function of NAT,ExtREAL such that
C7: ( 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 * F1) implies SMF1 . $1 = LL . $1 );
C8: S₁[ 0 ] by A2, C7;
C9: 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 * F1) ; :: thesis: SMF1 . (i + 1) = LL . (i + 1)
then SMF1 . (i + 1) = (SMF1 . i) + ((P * F1) . (i + 1)) by A2, NAT_1:13;
then SMF1 . (i + 1) = (LL . i) + ((Sum Mx) . (i + 1)) by C6, V1, V3, NAT_1:13;
hence SMF1 . (i + 1) = LL . (i + 1) by C7, V3, C2, NAT_1:13; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(C8, C9);
hence Sum (P * F1) = SumAll Mx by A2, C2, C7; :: thesis: verum