let M1, M2 be Matrix of ExtREAL; :: thesis: ( ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) implies (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) )
reconsider M = min ((len M1),(len M2)) as Element of NAT ;
assume B0: ( ( for i being Nat st i in dom M1 holds
not -infty in rng (M1 . i) ) & ( for i being Nat st i in dom M2 holds
not -infty in rng (M2 . i) ) ) ; :: thesis: (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
now :: thesis: not -infty in rng (Sum M1)
assume -infty in rng (Sum M1) ; :: thesis: contradiction
then consider i being Nat such that
C1: ( i in dom (Sum M1) & (Sum M1) . i = -infty ) by FINSEQ_2:10;
i in Seg (len (Sum M1)) by C1, FINSEQ_1:def 3;
then i in Seg (len M1) by Def5;
then i in dom M1 by FINSEQ_1:def 3;
then C2: not -infty in rng (M1 . i) by B0;
(Sum M1) . i = Sum (M1 . i) by C1, Def5;
then ex j being Nat st
( j in dom (M1 . i) & (M1 . i) . j = -infty ) by C1, Th17;
hence contradiction by C2, FUNCT_1:3; :: thesis: verum
end;
then D1: (Sum M1) " {-infty} = {} by FUNCT_1:72;
now :: thesis: not -infty in rng (Sum M2)
assume -infty in rng (Sum M2) ; :: thesis: contradiction
then consider i being Nat such that
C1: ( i in dom (Sum M2) & (Sum M2) . i = -infty ) by FINSEQ_2:10;
i in Seg (len (Sum M2)) by C1, FINSEQ_1:def 3;
then i in Seg (len M2) by Def5;
then i in dom M2 by FINSEQ_1:def 3;
then C2: not -infty in rng (M2 . i) by B0;
(Sum M2) . i = Sum (M2 . i) by C1, Def5;
then ex j being Nat st
( j in dom (M2 . i) & (M2 . i) . j = -infty ) by C1, Th17;
hence contradiction by C2, FUNCT_1:3; :: thesis: verum
end;
then (Sum M2) " {-infty} = {} by FUNCT_1:72;
then D2: (dom (Sum M1)) /\ (dom (Sum M2)) = ((dom (Sum M1)) /\ (dom (Sum M2))) \ ((((Sum M1) " {-infty}) /\ ((Sum M2) " {+infty})) \/ (((Sum M2) " {-infty}) /\ ((Sum M1) " {+infty}))) by D1;
A1: Seg M = (Seg (len M1)) /\ (Seg (len M2)) by FINSEQ_2:2
.= (Seg (len M1)) /\ (dom M2) by FINSEQ_1:def 3
.= (dom M1) /\ (dom M2) by FINSEQ_1:def 3
.= dom (M1 ^^ M2) by PRE_POLY:def 4
.= Seg (len (M1 ^^ M2)) by FINSEQ_1:def 3 ;
A0: ( dom (Sum M1) = Seg (len (Sum M1)) & dom (Sum M2) = Seg (len (Sum M2)) ) by FINSEQ_1:def 3;
dom ((Sum M1) + (Sum M2)) = (dom (Sum M1)) /\ (dom (Sum M2)) by D2, MESFUNC1:def 3;
then K1: dom ((Sum M1) + (Sum M2)) = Seg (min ((len (Sum M1)),(len (Sum M2)))) by A0, FINSEQ_2:2;
then reconsider SM12 = (Sum M1) + (Sum M2) as FinSequence by FINSEQ_1:def 2;
len SM12 = min ((len (Sum M1)),(len (Sum M2))) by K1, FINSEQ_1:def 3;
then A2: len SM12 = min ((len M1),(len (Sum M2))) by Def5
.= min ((len M1),(len M2)) by Def5
.= len (M1 ^^ M2) by A1, FINSEQ_1:6
.= len (Sum (M1 ^^ M2)) by Def5 ;
A3: dom ((Sum M1) + (Sum M2)) = Seg (len SM12) by FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom ((Sum M1) + (Sum M2)) holds
((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i
let i be Nat; :: thesis: ( i in dom ((Sum M1) + (Sum M2)) implies ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i )
assume A4: i in dom ((Sum M1) + (Sum M2)) ; :: thesis: ((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . i
then i in Seg (len SM12) by FINSEQ_1:def 3;
then i in Seg (len (M1 ^^ M2)) by A2, Def5;
then A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3;
then i in (dom M1) /\ (dom M2) by PRE_POLY:def 4;
then B1: ( i in dom M1 & i in dom M2 ) by XBOOLE_0:def 4;
then ( i in Seg (len M1) & i in Seg (len M2) ) by FINSEQ_1:def 3;
then ( i in Seg (len (Sum M1)) & i in Seg (len (Sum M2)) ) by Def5;
then A8: ( i in dom (Sum M1) & i in dom (Sum M2) ) by FINSEQ_1:def 3;
A10: i in dom (Sum (M1 ^^ M2)) by A2, A3, A4, FINSEQ_1:def 3;
A11: (M1 . i) ^ (M2 . i) = (M1 ^^ M2) . i by A6, PRE_POLY:def 4;
B3: ( not -infty in rng (M1 . i) & not -infty in rng (M2 . i) ) by B0, B1;
thus ((Sum M1) + (Sum M2)) . i = ((Sum M1) . i) + ((Sum M2) . i) by A4, MESFUNC1:def 3
.= (Sum (M1 . i)) + ((Sum M2) . i) by A8, Def5
.= (Sum (M1 . i)) + (Sum (M2 . i)) by A8, Def5
.= Sum ((M1 ^^ M2) . i) by A11, B3, EXTREAL1:10
.= (Sum (M1 ^^ M2)) . i by A10, Def5 ; :: thesis: verum
end;
hence (Sum M1) + (Sum M2) = Sum (M1 ^^ M2) by A2, FINSEQ_2:9; :: thesis: verum