let n be Element of NAT ; :: thesis: for A being Matrix of n, REAL st ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) holds
ex B being Matrix of n, REAL st B * A = 1_Rmatrix n
let A be Matrix of n, REAL ; :: thesis: ( ( for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ) implies ex B being Matrix of n, REAL st B * A = 1_Rmatrix n )
assume A1: for y being FinSequence of REAL st len y = n holds
ex x being FinSequence of REAL st
( len x = n & x * A = y ) ; :: thesis: ex B being Matrix of n, REAL st B * A = 1_Rmatrix n
A2: for i being Nat ex x being FinSequence of REAL st
( len x = n & x * A = Base_FinSeq n,i )

proof

let i be Nat; :: thesis: ex x being FinSequence of REAL st
( len x = n & x * A = Base_FinSeq n,i )
len (Base_FinSeq n,i) = n by Th74;
hence ex x being FinSequence of REAL st
( len x = n & x * A = Base_FinSeq n,i ) by A1; :: thesis: verum

end;

defpred S₁[ set , set ] means for s being Element of NAT
for q being FinSequence of REAL st s = $1 & q = $2 holds
( len q = n & q * A = Base_FinSeq n,s );
A3: for j being Nat st j in Seg n holds
ex d being Element of REAL * st S₁[j,d]

proof

let j be Nat; :: thesis: ( j in Seg n implies ex d being Element of REAL * st S₁[j,d] )
assume j in Seg n ; :: thesis: ex d being Element of REAL * st S₁[j,d]
consider x being FinSequence of REAL such that
A4: ( len x = n & x * A = Base_FinSeq n,j ) by A2;
reconsider d0 = x as Element of REAL * by FINSEQ_1:def 11;
for s being Element of NAT
for q being FinSequence of REAL st s = j & q = d0 holds
( len q = n & q * A = Base_FinSeq n,s ) by A4;
hence ex d being Element of REAL * st S₁[j,d] ; :: thesis: verum

end;

consider f being FinSequence of REAL * such that
A5: ( len f = n & ( for j being Nat st j in Seg n holds
S₁[j,f /. j] ) ) from FINSEQ_4:sch 1(A3);
for x being set st x in rng f holds
ex p being FinSequence of REAL st
( x = p & len p = n )

proof

let x be set ; :: thesis: ( x in rng f implies ex p being FinSequence of REAL st
( x = p & len p = n ) )
assume x in rng f ; :: thesis: ex p being FinSequence of REAL st
( x = p & len p = n )
then consider z being set such that
A6: ( z in dom f & f . z = x ) by FUNCT_1:def 5;
A7: z in Seg (len f) by A6, FINSEQ_1:def 3;
reconsider j0 = z as Element of NAT by A6;
reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def 11;
A8: ( len q0 = n & q0 * A = Base_FinSeq n,j0 ) by A5, A7;
q0 = x by A6, PARTFUN1:def 8;
hence ex p being FinSequence of REAL st
( x = p & len p = n ) by A8; :: thesis: verum

end;

then reconsider M = f as Matrix of REAL by MATRIX_1:9;
for p being FinSequence of REAL st p in rng M holds
len p = n

proof

let p be FinSequence of REAL ; :: thesis: ( p in rng M implies len p = n )
assume p in rng M ; :: thesis: len p = n
then consider z being set such that
A9: ( z in dom f & M . z = p ) by FUNCT_1:def 5;
A10: z in Seg (len f) by A9, FINSEQ_1:def 3;
reconsider j0 = z as Element of NAT by A9;
reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def 11;
q0 = p by A9, PARTFUN1:def 8;
hence len p = n by A5, A10; :: thesis: verum

end;

then reconsider B = M as Matrix of n, REAL by A5, MATRIX_1:def 3;
A11: for i4, j4 being Nat st [i4,j4] in Indices (B * A) holds
(B * A) * i4,j4 = (1_Rmatrix n) * i4,j4

proof

let i4, j4 be Nat; :: thesis: ( [i4,j4] in Indices (B * A) implies (B * A) * i4,j4 = (1_Rmatrix n) * i4,j4 )
assume A12: [i4,j4] in Indices (B * A) ; :: thesis: (B * A) * i4,j4 = (1_Rmatrix n) * i4,j4
reconsider i = i4, j = j4 as Element of NAT by ORDINAL1:def 13;
A13: [i,j] in [:(Seg n),(Seg n):] by A12, MATRIX_1:25;
then A14: [i,j] in Indices (1_Rmatrix n) by MATRIX_1:25;
A15: ( len (B * A) = n & ( for p being FinSequence of REAL st p in rng (B * A) holds
len p = n ) ) by MATRIX_1:def 3;
consider n2 being Nat such that
A16: for x being set st x in rng (M * A) holds
ex p being FinSequence of REAL st
( x = p & len p = n2 ) by MATRIX_1:9;
A17: ( i in dom (M * A) & j in Seg (width (M * A)) ) by A12, ZFMISC_1:106;
then A18: (M * A) . i in rng (M * A) by FUNCT_1:def 5;
then consider p2 being FinSequence of REAL such that
A19: ( (M * A) . i = p2 & len p2 = n2 ) by A16;
A20: ( 1 <= j & j <= width (M * A) ) by A17, FINSEQ_1:3;
consider p3 being FinSequence of REAL such that
A21: ( p3 = (1_Rmatrix n) . i & (1_Rmatrix n) * i,j = p3 . j ) by A14, MATRIX_1:def 6;
A22: ( i in Seg n & j in Seg n ) by A13, ZFMISC_1:106;
then A23: ( 1 <= i & i <= n ) by FINSEQ_1:3;
A24: ( 1 <= j & j <= n ) by A22, FINSEQ_1:3;
A25: ( len B = n & width B = n ) by MATRIX_1:25;
A26: ( len (B * A) = n & width (B * A) = n ) by MATRIX_1:25;

now

per cases ( i = j or i <> j ) ;

case A27: i = j ; :: thesis: (1_Rmatrix n) * i,j = p2 . j

then A28: (1_Rmatrix n) * i,j = (Base_FinSeq n,i) . i by A21, A23, Th78
.= 1 by A23, Th75 ;
len B = n by MATRIX_1:25;
then A29: f /. i = M . i by A23, FINSEQ_4:24;
reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def 11;
A30: ( len g = n & g * A = Base_FinSeq n,i ) by A5, A22;
A31: g = Line B,i by A23, A25, A29, Lm2;
p2 . j = (B * A) * i,j by A15, A18, A19, A20, A23, A26, Th2
.= (Base_FinSeq n,i) . j by A12, A30, A31, Th61
.= 1 by A23, A27, Th75 ;
hence (1_Rmatrix n) * i,j = p2 . j by A28; :: thesis: verum

end;

case A32: i <> j ; :: thesis: (1_Rmatrix n) * i,j = p2 . j

A33: (1_Rmatrix n) * i,j = (Base_FinSeq n,i) . j by A21, A23, Th78
.= 0 by A24, A32, Th76 ;
len B = n by MATRIX_1:25;
then A34: f /. i = M . i by A23, FINSEQ_4:24;
reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def 11;
g = Line B,i by A23, A25, A34, Lm2;
then A35: (Line B,i) * A = Base_FinSeq n,i by A5, A22;
p2 . j = (B * A) * i,j by A15, A18, A19, A20, A23, A26, Th2
.= (Base_FinSeq n,i) . j by A12, A35, Th61
.= 0 by A24, A32, Th76 ;
hence (1_Rmatrix n) * i,j = p2 . j by A33; :: thesis: verum

end;

end;

end;

hence (B * A) * i4,j4 = (1_Rmatrix n) * i4,j4 by A12, A19, MATRIX_1:def 6; :: thesis: verum

end;

reconsider M1 = B * A as Matrix of n,n, REAL ;
reconsider M2 = 1_Rmatrix n as Matrix of n,n, REAL ;
M1 = M2 by A11, MATRIX_1:28;
hence ex B being Matrix of n, REAL st B * A = 1_Rmatrix n ; :: thesis: verum