let V1, V2 be free finite-rank Z_Module; :: 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
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 ;
hence f1 = f2 by A1, A3, A6, Th22, FUNCT_1:2; :: thesis: verum