let R be Ring; :: thesis: for n being Nat
for A being invertible Matrix of n,R st n = 0 holds
ex z being Element of R st
( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) )
let n be Nat; :: thesis: for A being invertible Matrix of n,R st n = 0 holds
ex z being Element of R st
( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) )
let A be invertible Matrix of n,R; :: thesis: ( n = 0 implies ex z being Element of R st
( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) ) )
assume A1: n = 0 ; :: thesis: ex z being Element of R st
( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) )
take z = 1. R; :: thesis: ( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) )
A2: ( z in center (UnitGroup R) & z in center R & z in UnitGroup R )

proof

z = 1_ (UnitGroup R) by Th111;
hence z in center (UnitGroup R) by GROUP_2:46; :: thesis: ( z in center R & z in UnitGroup R )
z = 1_ R ;
hence z in center R by WEDDWITT:19; :: thesis: z in UnitGroup R
z = 1_ (UnitGroup R) by Th111;
hence z in UnitGroup R by STRUCT_0:def 5; :: thesis: verum

end;

A3: ( len A = len (z * (1. (R,n))) & width A = width (z * (1. (R,n))) )

proof

thus len A = n by MATRIX_0:25
.= len (z * (1. (R,n))) by MATRIX_0:25 ; :: thesis: width A = width (z * (1. (R,n)))
thus width A = n by MATRIX_0:24
.= width (z * (1. (R,n))) by MATRIX_0:24 ; :: thesis: verum

end;

for i, j being Nat st [i,j] in Indices A holds
A * (i,j) = (z * (1. (R,n))) * (i,j) by A1, MATRIX_0:22;
hence ( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) ) by A2, A3, MATRIX_0:21; :: thesis: verum