let n be Element of NAT ; :: thesis: for K being Field
for A being Matrix of n,K holds
( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )
let K be Field; :: thesis: for A being Matrix of n,K holds
( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )
let A be Matrix of n,K; :: thesis: ( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )

per cases ( n > 0 or n = 0 ) ;

suppose A1: n > 0 ; :: thesis: ( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )

thus ( ex B being Matrix of n,K st B * A = 1. K,n implies ex B2 being Matrix of n,K st A * B2 = 1. K,n ) by Th54; :: thesis: ( ex B2 being Matrix of n,K st A * B2 = 1. K,n implies ex B1 being Matrix of n,K st B1 * A = 1. K,n )
thus ( ex B being Matrix of n,K st A * B = 1. K,n implies ex B2 being Matrix of n,K st B2 * A = 1. K,n ) :: thesis: verum

proof

assume ex B being Matrix of n,K st A * B = 1. K,n ; :: thesis: ex B2 being Matrix of n,K st B2 * A = 1. K,n
then consider B being Matrix of n,K such that
A2: A * B = 1. K,n ;
A3: ( width A = n & len B = n ) by MATRIX_1:25;
( width B = n & (A * B) @ = 1. K,n ) by A2, MATRIX_1:25, MATRIX_6:10;
then (B @ ) * (A @ ) = 1. K,n by A1, A3, MATRIX_3:24;
then consider B2 being Matrix of n,K such that
A4: (A @ ) * B2 = 1. K,n by Th54;
A5: ( width (A @ ) = n & len B2 = n ) by MATRIX_1:25;
( width B2 = n & ((A @ ) * B2) @ = 1. K,n ) by A4, MATRIX_1:25, MATRIX_6:10;
then (B2 @ ) * ((A @ ) @ ) = 1. K,n by A1, A5, MATRIX_3:24;
then (B2 @ ) * A = 1. K,n by MATRIXR2:29;
hence ex B2 being Matrix of n,K st B2 * A = 1. K,n ; :: thesis: verum

end;

end;

suppose A6: n = 0 ; :: thesis: ( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n )

then A * A = 1. K,0 by Th15;
hence ( ex B1 being Matrix of n,K st B1 * A = 1. K,n iff ex B2 being Matrix of n,K st A * B2 = 1. K,n ) by A6; :: thesis: verum

end;

end;