let k, l, n be Nat; :: thesis: for K being comRing 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 comRing; :: 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