let V1, V2 be free finite-rank Z_Module; 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; 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; 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; ( 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
; 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
;
now for x being object st x in dom (f1 * b1) holds
(f1 * b1) . x = (f2 * b1) . xlet x be
object ;
( x in dom (f1 * b1) implies (f1 * b1) . x = (f2 * b1) . x )assume A7:
x in dom (f1 * b1)
;
(f1 * b1) . x = (f2 * b1) . xthen reconsider k =
x as
Nat ;
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
;
verum end;
hence
f1 = f2
by A1, A3, A6, Th22, FUNCT_1:2; verum