let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of finite-dimensional
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A, B being Matrix of the carrier of K, len b1, st Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 holds
A = B
let V1, V2 be finite-dimensional VectSp of finite-dimensional ; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for A, B being Matrix of the carrier of K, len b1, 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 the carrier of K, len b1, 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 the carrier of K, len b1, st Mx2Tran A,b1,b2 = Mx2Tran B,b1,b2 holds
A = B
let A, B be Matrix of the carrier of K, len b1,; :: 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