let R be Ring; :: thesis: Matrix_ring (1,R),R are_isomorphic
set UR = the carrier of R;
defpred S₁[ object , object ] means $2 = <*<*$1*>*>;
A1: for x being Element of the carrier of R ex y being Element of 1 -Matrices_over R st S₁[x,y]

proof

let x be Element of the carrier of R; :: thesis: ex y being Element of 1 -Matrices_over R st S₁[x,y]
reconsider x0 = x as Element of R ;
consider y being Matrix of 1,R such that
A2: y = <*<*x0*>*> ;
reconsider y = y as Element of 1 -Matrices_over R by MATRIX_1:2;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A2; :: thesis: verum

end;

consider f being Function of the carrier of R,(1 -Matrices_over R) such that
A3: for r being Element of the carrier of R holds S₁[r,f . r] from FUNCT_2:sch 3(A1);
reconsider f = f as Function of R,(Matrix_ring (1,R)) ;
A4: f is onto

proof

for y being object st y in the carrier of (Matrix_ring (1,R)) holds
ex x being object st
( x in the carrier of R & y = f . x )

proof

let y be object ; :: thesis: ( y in the carrier of (Matrix_ring (1,R)) implies ex x being object st
( x in the carrier of R & y = f . x ) )
assume y in the carrier of (Matrix_ring (1,R)) ; :: thesis: ex x being object st
( x in the carrier of R & y = f . x )
then reconsider M = y as Matrix of 1,R by Th72;
take x = M * (1,1); :: thesis: ( x in the carrier of R & y = f . x )
thus x in the carrier of R ; :: thesis: y = f . x
thus y = <*<*x*>*> by Th33
.= f . x by A3 ; :: thesis: verum

end;

then rng f = the carrier of (Matrix_ring (1,R)) by FUNCT_2:10;
hence f is onto by FUNCT_2:def 3; :: thesis: verum

end;

A5: f is one-to-one

proof

for a, b being Element of R st f . a = f . b holds
a = b

proof

let a, b be Element of R; :: thesis: ( f . a = f . b implies a = b )
assume A6: f . a = f . b ; :: thesis: a = b
A7: <*<*a*>*> = f . b by A3, A6
.= <*<*b*>*> by A3 ;
{[1,<*a*>]} = <*<*a*>*> by FINSEQ_1:37
.= {[1,<*b*>]} by A7, FINSEQ_1:37 ;
then [1,<*a*>] = [1,<*b*>] by ZFMISC_1:3;
then A8: <*a*> = <*b*> by XTUPLE_0:1;
{[1,a]} = <*a*> by FINSEQ_1:37
.= {[1,b]} by A8, FINSEQ_1:37 ;
then [1,a] = [1,b] by ZFMISC_1:3;
hence a = b by XTUPLE_0:1; :: thesis: verum

end;

hence f is one-to-one by GROUP_6:1; :: thesis: verum

end;

f is linear

proof

for x, y being Element of R holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Element of R; :: thesis: f . (x + y) = (f . x) + (f . y)
reconsider M1 = f . x, M2 = f . y as Matrix of 1,R by Th72;
A9: ( M1 = <*<*x*>*> & M2 = <*<*y*>*> ) by A3;
thus (f . x) + (f . y) = M1 + M2 by Th73
.= <*<*(x + y)*>*> by A9, Th36
.= f . (x + y) by A3 ; :: thesis: verum

end;

then A10: f is additive by VECTSP_1:def 20;

now :: thesis: for x, y being Element of R holds (f . x) * (f . y) = f . (x * y)

let x, y be Element of R; :: thesis: (f . x) * (f . y) = f . (x * y)
reconsider M1 = f . x, M2 = f . y as Matrix of 1,R by Th72;
A11: ( M1 = <*<*x*>*> & M2 = <*<*y*>*> ) by A3;
thus (f . x) * (f . y) = M1 * M2 by Th75
.= <*<*(x * y)*>*> by A11, Th35
.= f . (x * y) by A3 ; :: thesis: verum

end;

then A12: f is multiplicative by GROUP_6:def 6;
f is unity-preserving

proof

f . (1_ R) = <*<*(1_ R)*>*> by A3
.= 1_ (Matrix_ring (1,R)) by Th34 ;
hence f is unity-preserving by GROUP_1:def 13; :: thesis: verum

end;

hence f is linear by A10, A12; :: thesis: verum

end;

hence Matrix_ring (1,R),R are_isomorphic by A4, A5, QUOFIELD:def 23; :: thesis: verum