let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A, B being Matrix of len b1, len b2,K st Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 holds
A = B
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A, B being Matrix of len b1, len b2,K st Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 holds
A = B
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2
for A, B being Matrix of len b1, len b2,K st Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 holds
A = B
let b2 be OrdBasis of V2; :: thesis: for A, B being Matrix of len b1, len b2,K st Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 holds
A = B
let A, B be Matrix of len b1, len b2,K; :: thesis: ( Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 implies A = B )
assume Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 ; :: thesis: A = B
hence A = AutMt (Mx2Tran B,b1,b2),b1,b2 by Th36
.= B by Th36 ;
:: thesis: verum