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 ;

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

hence
f1 = f2
by A1, A3, A6, Th22, FUNCT_1:2; :: thesis: verum(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;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