let R be Ring; :: thesis: for Y being Matrix of 1,R holds Y = (Y * (1,1)) * (1. (R,1))
let Y be Matrix of 1,R; :: thesis: Y = (Y * (1,1)) * (1. (R,1))
for i, j being Nat st [i,j] in Indices Y holds
Y * (i,j) = ((Y * (1,1)) * (1. (R,1))) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices Y implies Y * (i,j) = ((Y * (1,1)) * (1. (R,1))) * (i,j) )
assume A1: [i,j] in Indices Y ; :: thesis: Y * (i,j) = ((Y * (1,1)) * (1. (R,1))) * (i,j)
A2: Indices Y = [:(Seg 1),(Seg 1):] by MATRIX_0:24
.= Indices (1. (R,1)) by MATRIX_0:24 ;
A3: ( i = 1 & j = 1 )

proof

[i,j] in [:(Seg 1),(Seg 1):] by A1, MATRIX_0:24;
then ( i in Seg 1 & j in Seg 1 ) by ZFMISC_1:87;
hence ( i = 1 & j = 1 ) by FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;

set Y11 = Y * (1,1);
thus Y * (i,j) = (Y * (1,1)) * (1. R) by A3
.= (Y * (1,1)) * ((1. (R,1)) * (1,1)) by A1, A2, A3, MATRIX_1:def 3
.= ((Y * (1,1)) * (1. (R,1))) * (i,j) by A1, A2, A3, MATRIX_3:def 5 ; :: thesis: verum

end;

hence Y = (Y * (1,1)) * (1. (R,1)) by MATRIX_0:27; :: thesis: verum