let n be 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 )
defpred S₁[ set , set ] means for s being Nat
for q being FinSequence of REAL st s = $1 & q = $2 holds
( len q = n & q * A = Base_FinSeq (n,s) );
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;

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 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 object st x in rng f holds
ex p being FinSequence of REAL st
( x = p & len p = n )

proof

let x be object ; :: 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 object such that
A6: z in dom f and
A7: f . z = x by FUNCT_1:def 3;
reconsider j0 = z as Nat by A6;
reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def 11;
z in Seg (len f) by A6, FINSEQ_1:def 3;
then A8: len q0 = n by A5;
q0 = x by A6, A7, PARTFUN1:def 6;
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_0: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 object such that
A9: z in dom f and
A10: M . z = p by FUNCT_1:def 3;
reconsider j0 = z as Nat by A9;
reconsider q0 = f /. j0 as FinSequence of REAL by FINSEQ_1:def 11;
( z in Seg (len f) & q0 = p ) by A9, A10, FINSEQ_1:def 3, PARTFUN1:def 6;
hence len p = n by A5; :: thesis: verum

end;

then reconsider B = M as Matrix of n,REAL by A5, MATRIX_0:def 2;
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) )
reconsider i = i4, j = j4 as Nat ;
consider n2 being Nat such that
A11: for x being object st x in rng (M * A) holds
ex p being FinSequence of REAL st
( x = p & len p = n2 ) by MATRIX_0:9;
assume A12: [i4,j4] in Indices (B * A) ; :: thesis: (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4)
then j in Seg (width (M * A)) by ZFMISC_1:87;
then A13: ( 1 <= j & j <= width (M * A) ) by FINSEQ_1:1;
i in dom (M * A) by A12, ZFMISC_1:87;
then A14: (M * A) . i in rng (M * A) by FUNCT_1:def 3;
then consider p2 being FinSequence of REAL such that
A15: (M * A) . i = p2 and
A16: len p2 = n2 by A11;
A17: len B = n by MATRIX_0:24;
A18: [i,j] in [:(Seg n),(Seg n):] by A12, MATRIX_0:24;
then [i,j] in Indices (1_Rmatrix n) by MATRIX_0:24;
then A19: ex p3 being FinSequence of REAL st
( p3 = (1_Rmatrix n) . i & (1_Rmatrix n) * (i,j) = p3 . j ) by MATRIX_0:def 5;
A20: width (B * A) = n by MATRIX_0:24;
j in Seg n by A18, ZFMISC_1:87;
then A21: ( 1 <= j & j <= n ) by FINSEQ_1:1;
A22: i in Seg n by A18, ZFMISC_1:87;
then A23: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A24: ( len (B * A) = n & ( for p being FinSequence of REAL st p in rng (B * A) holds
len p = n ) ) by MATRIX_0:def 2;

now :: thesis: ( ( i = j & (1_Rmatrix n) * (i,j) = p2 . j ) or ( i <> j & (1_Rmatrix n) * (i,j) = p2 . j ) )

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

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

reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def 11;
A26: g * A = Base_FinSeq (n,i) by A5, A22;
len B = n by MATRIX_0:24;
then f /. i = M . i by A23, FINSEQ_4:15;
then A27: g = Line (B,i) by A23, A17, Lm2;
A28: (1_Rmatrix n) * (i,j) = (Base_FinSeq (n,i)) . i by A19, A23, A25, Th78
.= 1 by A23, Th75 ;
p2 . j = (B * A) * (i,j) by A24, A14, A15, A16, A13, A23, A20, Th2
.= (Base_FinSeq (n,i)) . j by A12, A26, A27, Th61
.= 1 by A23, A25, Th75 ;
hence (1_Rmatrix n) * (i,j) = p2 . j by A28; :: thesis: verum

end;

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

reconsider g = f /. i as FinSequence of REAL by FINSEQ_1:def 11;
len B = n by MATRIX_0:24;
then f /. i = M . i by A23, FINSEQ_4:15;
then g = Line (B,i) by A23, A17, Lm2;
then A30: (Line (B,i)) * A = Base_FinSeq (n,i) by A5, A22;
A31: (1_Rmatrix n) * (i,j) = (Base_FinSeq (n,i)) . j by A19, A23, Th78
.= 0 by A21, A29, Th76 ;
p2 . j = (B * A) * (i,j) by A24, A14, A15, A16, A13, A23, A20, Th2
.= (Base_FinSeq (n,i)) . j by A12, A30, Th61
.= 0 by A21, A29, Th76 ;
hence (1_Rmatrix n) * (i,j) = p2 . j by A31; :: thesis: verum

end;

end;

end;

hence (B * A) * (i4,j4) = (1_Rmatrix n) * (i4,j4) by A12, A15, MATRIX_0:def 5; :: thesis: verum

end;

hence ex B being Matrix of n,REAL st B * A = 1_Rmatrix n by MATRIX_0:27; :: thesis: verum