let D be non empty set ; :: thesis: for d1, d2 being Element of D
for M1, M2, N1, N2 being Matrix of D st len M1 = len N1 & width M1 = width N1 & len M2 = len N2 & width M2 = width N2 & block_diagonal (<*M1,M2*>,d1) = block_diagonal (<*N1,N2*>,d2) holds
( M1 = N1 & M2 = N2 )
let d1, d2 be Element of D; :: thesis: for M1, M2, N1, N2 being Matrix of D st len M1 = len N1 & width M1 = width N1 & len M2 = len N2 & width M2 = width N2 & block_diagonal (<*M1,M2*>,d1) = block_diagonal (<*N1,N2*>,d2) holds
( M1 = N1 & M2 = N2 )
let M1, M2, N1, N2 be Matrix of D; :: thesis: ( len M1 = len N1 & width M1 = width N1 & len M2 = len N2 & width M2 = width N2 & block_diagonal (<*M1,M2*>,d1) = block_diagonal (<*N1,N2*>,d2) implies ( M1 = N1 & M2 = N2 ) )
assume that
A1: len M1 = len N1 and
A2: width M1 = width N1 and
A3: len M2 = len N2 and
A4: width M2 = width N2 and
A5: block_diagonal (<*M1,M2*>,d1) = block_diagonal (<*N1,N2*>,d2) ; :: thesis: ( M1 = N1 & M2 = N2 )
set G1 = <*N1*>;
set F1 = <*M1*>;
reconsider W1 = width M1 as Element of NAT by ORDINAL1:def 12;
A6: Sum (Width <*M1*>) = Sum <*W1*> by Th19
.= Sum (Width <*N1*>) by A2, Th19 ;
set G2 = <*N2*>;
set F2 = <*M2*>;
thus M1 = Segm ((block_diagonal ((<*M1*> ^ <*M2*>),d1)),(Seg (len M1)),(Seg (width M1))) by Th32
.= Segm ((block_diagonal ((<*N1*> ^ <*N2*>),d2)),(Seg (len N1)),(Seg (width N1))) by A1, A2, A5
.= N1 by Th32 ; :: thesis: M2 = N2
A7: Sum (Len <*M1*>) = Sum <*(len M1)*> by Th15
.= Sum (Len <*N1*>) by A1, Th15 ;
thus M2 = Segm ((block_diagonal ((<*M1*> ^ <*M2*>),d1)),((Seg ((len M2) + (Sum (Len <*M1*>)))) \ (Seg (Sum (Len <*M1*>)))),((Seg ((width M2) + (Sum (Width <*M1*>)))) \ (Seg (Sum (Width <*M1*>))))) by Th33
.= N2 by A3, A4, A5, A7, A6, Th33 ; :: thesis: verum