let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f1 is linear & f2 is linear & AutMt f1,b1,b2 = AutMt f2,b1,b2 & len b1 > 0 holds
f1 = f2
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for f1, f2 being Function of V1,V2
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f1 is linear & f2 is linear & AutMt f1,b1,b2 = AutMt f2,b1,b2 & len b1 > 0 holds
f1 = f2
let f1, f2 be Function of V1,V2; :: thesis: for b1 being OrdBasis of V1
for b2 being OrdBasis of V2 st f1 is linear & f2 is linear & AutMt f1,b1,b2 = AutMt f2,b1,b2 & len b1 > 0 holds
f1 = f2
let b1 be OrdBasis of V1; :: thesis: for b2 being OrdBasis of V2 st f1 is linear & f2 is linear & AutMt f1,b1,b2 = AutMt f2,b1,b2 & len b1 > 0 holds
f1 = f2
let b2 be OrdBasis of V2; :: thesis: ( f1 is linear & f2 is linear & AutMt f1,b1,b2 = AutMt f2,b1,b2 & len b1 > 0 implies f1 = f2 )
assume that
A1: ( f1 is linear & f2 is linear ) and
A2: AutMt f1,b1,b2 = AutMt f2,b1,b2 and
A3: len b1 > 0 ; :: thesis: f1 = f2
rng b1 is Basis of V1 by Def4;
then A4: rng b1 c= the carrier of V1 ;
then A5: rng b1 c= dom f2 by FUNCT_2:def 1;
rng b1 c= dom f1 by A4, FUNCT_2:def 1;
then A6: dom (f1 * b1) = dom b1 by RELAT_1:46
.= dom (f2 * b1) by A5, RELAT_1:46 ;

now

let x be set ; :: thesis: ( x in dom (f1 * b1) implies (f1 * b1) . x = (f2 * b1) . x )
assume A7: x in dom (f1 * b1) ; :: thesis: (f1 * b1) . x = (f2 * b1) . x
then reconsider k = x as Nat by FINSEQ_3:25;
A8: dom (f1 * b1) c= dom b1 by RELAT_1:44;
then A9: (f1 . (b1 /. k)) |-- b2 = (AutMt f2,b1,b2) /. k by A2, A7, Def10
.= (f2 . (b1 /. k)) |-- b2 by A7, A8, Def10 ;
thus (f1 * b1) . x = f1 . (b1 . x) by A7, FUNCT_1:22
.= f1 . (b1 /. x) by A7, A8, PARTFUN1:def 8
.= f2 . (b1 /. x) by A9, Th39
.= f2 . (b1 . x) by A7, A8, PARTFUN1:def 8
.= (f2 * b1) . x by A6, A7, FUNCT_1:22 ; :: thesis: verum

end;

hence f1 = f2 by A1, A3, A6, Th26, FUNCT_1:9; :: thesis: verum