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