let 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)) & n > 0 holds
A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,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)) & n > 0 holds
A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a)
let a be Element of K; for A being Matrix of n,K st l in dom (1. (K,n)) & n > 0 holds
A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a)
let A be Matrix of n,K; ( l in dom (1. (K,n)) & n > 0 implies A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a) )
assume that
A1:
l in dom (1. (K,n))
and
A2:
n > 0
; A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,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 (SXLine ((1. (K,n)),l,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;
(SXLine ((A @),l,a)) @ =
((SXLine ((1. (K,n)),l,a)) * (A @)) @
by A1, Th7
.=
((A @) @) * ((SXLine ((1. (K,n)),l,a)) @)
by A2, A4, A7, A6, MATRIX_3:22
.=
A * ((SXLine ((1. (K,n)),l,a)) @)
by A2, A8, A9, MATRIX_0:57
.=
A * ((SXLine (((1. (K,n)) @),l,a)) @)
by MATRIX_6:10
.=
A * (SXCol ((1. (K,n)),l,a))
by A1, A2, A5, Th16
;
hence
A * (SXCol ((1. (K,n)),l,a)) = SXCol (A,l,a)
by A1, A2, A10, Th16; verum