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 additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & 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 additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & 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 additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & 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 additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 holds
f1 = f2
let b2 be OrdBasis of V2; :: thesis: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & AutMt (f1,b1,b2) = AutMt (f2,b1,b2) & len b1 > 0 implies f1 = f2 )
assume that
A1: ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous ) 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 Def2;
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:27
.= dom (f2 * b1) by A5, RELAT_1:27 ;

now :: thesis: for x being object st x in dom (f1 * b1) holds
(f1 * b1) . x = (f2 * b1) . x

let x be object ; :: 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:23;
A8: dom (f1 * b1) c= dom b1 by RELAT_1:25;
then A9: (f1 . (b1 /. k)) |-- b2 = (AutMt (f2,b1,b2)) /. k by A2, A7, Def8
.= (f2 . (b1 /. k)) |-- b2 by A7, A8, Def8 ;
thus (f1 * b1) . x = f1 . (b1 . x) by A7, FUNCT_1:12
.= f1 . (b1 /. x) by A7, A8, PARTFUN1:def 6
.= f2 . (b1 /. x) by A9, Th34
.= f2 . (b1 . x) by A7, A8, PARTFUN1:def 6
.= (f2 * b1) . x by A6, A7, FUNCT_1:12 ; :: thesis: verum

end;

hence f1 = f2 by A1, A3, A6, Th22, FUNCT_1:2; :: thesis: verum