let l, n be Nat; :: thesis: for K being Field
for a being Element of K st l in dom (1. K,n) & a <> 0. K & n > 0 holds
(SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " )
let K be Field; :: thesis: for a being Element of K st l in dom (1. K,n) & a <> 0. K & n > 0 holds
(SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " )
let a be Element of K; :: thesis: ( l in dom (1. K,n) & a <> 0. K & n > 0 implies (SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " ) )
assume that
A1: l in dom (1. K,n) and
A2: a <> 0. K and
A3: n > 0 ; :: thesis: (SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " )
A4: (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) by A1, A2, Th14;
( len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
then A5: dom (1. K,n) = Seg (width (1. K,n)) by FINSEQ_1:def 3;
(1. K,n) @ = 1. K,n by MATRIX_6:10;
then SXCol (1. K,n),l,(a " ) = (SXLine (1. K,n),l,(a " )) @ by A1, A3, A5, Th16
.= ((SXLine (1. K,n),l,a) @ ) ~ by A1, A2, A3, A4, Th14, MATRIX_6:13
.= ((SXLine ((1. K,n) @ ),l,a) @ ) ~ by MATRIX_6:10
.= (SXCol (1. K,n),l,a) ~ by A1, A3, A5, Th16 ;
hence (SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " ) ; :: thesis: verum