let l, n, k be Nat; :: thesis: for K being Field st l in dom (1. K,n) & k in dom (1. K,n) holds
( ILine (1. K,n),l,k is invertible & (ILine (1. K,n),l,k) ~ = ILine (1. K,n),l,k )
let K be Field; :: thesis: ( l in dom (1. K,n) & k in dom (1. K,n) implies ( ILine (1. K,n),l,k is invertible & (ILine (1. K,n),l,k) ~ = ILine (1. K,n),l,k ) )
assume ( l in dom (1. K,n) & k in dom (1. K,n) ) ; :: thesis: ( ILine (1. K,n),l,k is invertible & (ILine (1. K,n),l,k) ~ = ILine (1. K,n),l,k )
then ( (ILine (1. K,n),l,k) * (ILine (1. K,n),l,k) = ILine (ILine (1. K,n),l,k),l,k & ILine (ILine (1. K,n),l,k),l,k = 1. K,n ) by Th6, Th11;
then A1: ILine (1. K,n),l,k is_reverse_of ILine (1. K,n),l,k by MATRIX_6:def 2;
then ILine (1. K,n),l,k is invertible by MATRIX_6:def 3;
hence ( ILine (1. K,n),l,k is invertible & (ILine (1. K,n),l,k) ~ = ILine (1. K,n),l,k ) by A1, MATRIX_6:def 4; :: thesis: verum