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 A1: ( l in dom (1. K,n) & a <> 0. K & n > 0 ) ; :: thesis: (SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " )
A2: (1. K,n) @ = 1. K,n by MATRIX_6:10;
( len (1. K,n) = n & width (1. K,n) = n ) by MATRIX_1:25;
then A3: dom (1. K,n) = Seg (width (1. K,n)) by FINSEQ_1:def 3;
A4: ( SXLine (1. K,n),l,a is invertible & (SXLine (1. K,n),l,a) ~ = SXLine (1. K,n),l,(a " ) ) by A1, Th14;
SXCol (1. K,n),l,(a " ) = (SXLine (1. K,n),l,(a " )) @ by A1, A2, A3, Th16, VECTSP_2:48
.= ((SXLine (1. K,n),l,a) @ ) ~ by A1, A4, MATRIX_6:13
.= ((SXLine ((1. K,n) @ ),l,a) @ ) ~ by MATRIX_6:10
.= (SXCol (1. K,n),l,a) ~ by A1, A3, Th16 ;
hence (SXCol (1. K,n),l,a) ~ = SXCol (1. K,n),l,(a " ) ; :: thesis: verum