let V1 be free finite-rank Z_Module; for M1, M2 being Matrix of the carrier of V1 holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
let M1, M2 be Matrix of the carrier of V1; (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
reconsider m = min ((len M1),(len M2)) as Element of NAT by ORDINAL1:def 12;
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
;
A2: len ((Sum M1) + (Sum M2)) =
min ((len (Sum M1)),(len (Sum M2)))
by FINSEQ_2:71
.=
min ((len M1),(len (Sum M2)))
by MATRLIN:def 6
.=
min ((len M1),(len M2))
by MATRLIN:def 6
.=
len (M1 ^^ M2)
by A1, FINSEQ_1:6
.=
len (Sum (M1 ^^ M2))
by MATRLIN:def 6
;
A3:
dom ((Sum M1) + (Sum M2)) = Seg (len ((Sum M1) + (Sum M2)))
by FINSEQ_1:def 3;
now for i being Nat st i in dom ((Sum M1) + (Sum M2)) holds
((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . ilet i be
Nat;
( 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))
;
((Sum M1) + (Sum M2)) . i = (Sum (M1 ^^ M2)) . ithen A5:
i in dom (Sum (M1 ^^ M2))
by A2, A3, FINSEQ_1:def 3;
i in Seg (len (M1 ^^ M2))
by A2, A3, A4, MATRLIN:def 6;
then A6:
i in dom (M1 ^^ M2)
by FINSEQ_1:def 3;
then A7:
i in (dom M1) /\ (dom M2)
by PRE_POLY:def 4;
then A8:
i in dom M1
by XBOOLE_0:def 4;
A9:
i in dom M2
by A7, XBOOLE_0:def 4;
reconsider m1 =
M1 . i,
m2 =
M2 . i as
FinSequence ;
A10:
(M1 /. i) ^ (M2 /. i) =
m1 ^ (M2 /. i)
by A8, PARTFUN1:def 6
.=
m1 ^ m2
by A9, PARTFUN1:def 6
.=
(M1 ^^ M2) . i
by A6, PRE_POLY:def 4
.=
(M1 ^^ M2) /. i
by A6, PARTFUN1:def 6
;
i in Seg (len M2)
by A9, FINSEQ_1:def 3;
then
i in Seg (len (Sum M2))
by MATRLIN:def 6;
then A11:
i in dom (Sum M2)
by FINSEQ_1:def 3;
then A12:
(Sum M2) /. i = (Sum M2) . i
by PARTFUN1:def 6;
i in Seg (len M1)
by A8, FINSEQ_1:def 3;
then
i in Seg (len (Sum M1))
by MATRLIN:def 6;
then A13:
i in dom (Sum M1)
by FINSEQ_1:def 3;
then
(Sum M1) /. i = (Sum M1) . i
by PARTFUN1:def 6;
hence ((Sum M1) + (Sum M2)) . i =
((Sum M1) /. i) + ((Sum M2) /. i)
by A4, A12, FUNCOP_1:22
.=
(Sum (M1 /. i)) + ((Sum M2) /. i)
by A13, MATRLIN:def 6
.=
(Sum (M1 /. i)) + (Sum (M2 /. i))
by A11, MATRLIN:def 6
.=
Sum ((M1 ^^ M2) /. i)
by A10, RLVECT_1:41
.=
(Sum (M1 ^^ M2)) /. i
by A5, MATRLIN:def 6
.=
(Sum (M1 ^^ M2)) . i
by A5, PARTFUN1:def 6
;
verum end;
hence
(Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
by A2, FINSEQ_2:9; verum