let k, l, n be Nat; :: thesis: for K being Field st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
(ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k)
let K be Field; :: thesis: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 implies (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k) )
assume that
A1: ( l in dom (1. (K,n)) & k in dom (1. (K,n)) ) and
A2: n > 0 ; :: thesis: (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k)
A3: (ILine ((1. (K,n)),l,k)) ~ = ILine ((1. (K,n)),l,k) by A1, Th12;
a2: ILine ((1. (K,n)),l,k) is invertible by A1, Th12;
( len (1. (K,n)) = n & width (1. (K,n)) = n ) by MATRIX_0:24;
then A4: 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 ICol ((1. (K,n)),l,k) = (ILine ((1. (K,n)),l,k)) @ by A1, A2, A4, Th15
.= ((ILine ((1. (K,n)),l,k)) @) ~ by A3, MATRIX_6:13, a2
.= ((ILine (((1. (K,n)) @),l,k)) @) ~ by MATRIX_6:10
.= (ICol ((1. (K,n)),l,k)) ~ by A1, A2, A4, Th15 ;
hence (ICol ((1. (K,n)),l,k)) ~ = ICol ((1. (K,n)),l,k) ; :: thesis: verum