let k, l, n be Nat; for K being Field
for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)
let K be Field; for a being Element of K
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)
let a be Element of K; for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)
let A be Matrix of n,K; ( l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 implies A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a) )
assume that
A1:
( l in dom (1. (K,n)) & k in dom (1. (K,n)) )
and
A2:
n > 0
; A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)
A3:
len (1. (K,n)) = n
by MATRIX_0:24;
A4:
width (1. (K,n)) = n
by MATRIX_0:24;
then A5:
dom (1. (K,n)) = Seg (width (1. (K,n)))
by A3, FINSEQ_1:def 3;
A6:
width (A @) = n
by MATRIX_0:24;
A7:
( width (RLineXS ((1. (K,n)),l,k,a)) = width (1. (K,n)) & len (A @) = n )
by Th1, MATRIX_0:24;
A8:
len A = n
by MATRIX_0:24;
A9:
width A = n
by MATRIX_0:24;
then A10:
Seg (width A) = dom (1. (K,n))
by A3, FINSEQ_1:def 3;
(RLineXS ((A @),l,k,a)) @ =
((RLineXS ((1. (K,n)),l,k,a)) * (A @)) @
by A1, Th8
.=
((A @) @) * ((RLineXS ((1. (K,n)),l,k,a)) @)
by A2, A4, A7, A6, MATRIX_3:22
.=
A * ((RLineXS ((1. (K,n)),l,k,a)) @)
by A2, A8, A9, MATRIX_0:57
.=
A * ((RLineXS (((1. (K,n)) @),l,k,a)) @)
by MATRIX_6:10
.=
A * (RColXS ((1. (K,n)),l,k,a))
by A1, A2, A5, Th17
;
hence
A * (RColXS ((1. (K,n)),l,k,a)) = RColXS (A,l,k,a)
by A1, A2, A10, Th17; verum