let n be Nat; :: thesis: for A, B being Matrix of n,F_Real st Det A <> 0. F_Real holds
( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )
A1: ( n = 0 implies n = 0 ) ;
let A, B be Matrix of n,F_Real; :: thesis: ( Det A <> 0. F_Real implies ( (Mx2Tran A) " = Mx2Tran B iff A ~ = B ) )
assume A2: Det A <> 0. F_Real ; :: thesis: ( (Mx2Tran A) " = Mx2Tran B iff A ~ = B )
A3: A is invertible by A2, LAPLACE:34;
set MA = Mx2Tran A;
set MB = Mx2Tran B;
A4: width B = n by MATRIX_0:24;
reconsider ma = Mx2Tran A, mb = Mx2Tran B as Function ;
A5: ( width A = n & len A = n ) by MATRIX_0:24;
A6: Mx2Tran A is one-to-one by A2, Th40;
hereby :: thesis: ( A ~ = B implies (Mx2Tran A) " = Mx2Tran B )
assume (Mx2Tran A) " = Mx2Tran B ; :: thesis: A ~ = B
then A7: mb * ma = id (dom ma) by A6, FUNCT_1:39
.= id (TOP-REAL n) by FUNCT_2:def 1
.= Mx2Tran (1. (F_Real,n)) by Th33 ;
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) by A5, A4, A1, Th32;
then B is_reverse_of A by A3, A7, Th34, MATRIX_6:38;
hence A ~ = B by A3, MATRIX_6:def 4; :: thesis: verum
end;
assume A8: A ~ = B ; :: thesis: (Mx2Tran A) " = Mx2Tran B
Mx2Tran A is onto by A2, Th42;
then A9: ( dom (Mx2Tran B) = [#] (TOP-REAL n) & rng (Mx2Tran A) = [#] (TOP-REAL n) ) by FUNCT_2:def 1, FUNCT_2:def 3;
A10: n in NAT by ORDINAL1:def 12;
(Mx2Tran B) * (Mx2Tran A) = Mx2Tran (A * B) by A5, A4, A1, Th32
.= Mx2Tran (1. (F_Real,n)) by A3, A10, A8, MATRIX14:18
.= id (TOP-REAL n) by Th33
.= id (dom (Mx2Tran A)) by FUNCT_2:def 1 ;
hence (Mx2Tran A) " = Mx2Tran B by A6, A9, FUNCT_1:41; :: thesis: verum