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;
a3: SXLine ((1. (K,n)),l,a) is invertible by A1, A2, Th14;
( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_0:24;
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 A4, MATRIX_6:13, a3
.= ((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