let n be Nat; :: thesis: 1. (INT.Ring,n) = 1. (F_Real,n)
set M = 1. (INT.Ring,n);
set L = 1. (F_Real,n);
P1: ( len (1. (INT.Ring,n)) = n & width (1. (INT.Ring,n)) = n & Indices (1. (INT.Ring,n)) = [:(Seg n),(Seg n):] ) by MATRIX_0:24;
P2: ( len (1. (F_Real,n)) = n & width (1. (F_Real,n)) = n & Indices (1. (F_Real,n)) = [:(Seg n),(Seg n):] ) by MATRIX_0:24;
for i, j being Nat st [i,j] in Indices (1. (INT.Ring,n)) holds
(1. (INT.Ring,n)) * (i,j) = (1. (F_Real,n)) * (i,j)
proof
let i, j be Nat; :: thesis: ( [i,j] in Indices (1. (INT.Ring,n)) implies (1. (INT.Ring,n)) * (i,j) = (1. (F_Real,n)) * (i,j) )
assume AS: [i,j] in Indices (1. (INT.Ring,n)) ; :: thesis: (1. (INT.Ring,n)) * (i,j) = (1. (F_Real,n)) * (i,j)
per cases ( i = j or i <> j ) ;
suppose Q1: i = j ; :: thesis: (1. (INT.Ring,n)) * (i,j) = (1. (F_Real,n)) * (i,j)
hence (1. (INT.Ring,n)) * (i,j) = 1. INT.Ring by MATRIX_1:def 3, AS
.= 1. F_Real
.= (1. (F_Real,n)) * (i,j) by Q1, MATRIX_1:def 3, P1, P2, AS ;
:: thesis: verum
end;
suppose Q2: i <> j ; :: thesis: (1. (INT.Ring,n)) * (i,j) = (1. (F_Real,n)) * (i,j)
hence (1. (INT.Ring,n)) * (i,j) = 0. INT.Ring by MATRIX_1:def 3, AS
.= 0. F_Real
.= (1. (F_Real,n)) * (i,j) by Q2, MATRIX_1:def 3, P1, P2, AS ;
:: thesis: verum
end;
end;
end;
hence 1. (INT.Ring,n) = 1. (F_Real,n) by P1, P2, ZMATRLIN:4; :: thesis: verum