let V1, V2 be free finite-rank Z_Module; for f1, f2 being Function of V1,V2 st f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous holds
for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds
f1 = f2
let f1, f2 be Function of V1,V2; ( f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous implies for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds
f1 = f2 )
assume that
A1:
( f1 is additive & f1 is homogeneous )
and
A2:
( f2 is additive & f2 is homogeneous )
; for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds
f1 = f2
let b1 be OrdBasis of V1; ( len b1 > 0 & f1 * b1 = f2 * b1 implies f1 = f2 )
assume A3:
len b1 > 0
; ( not f1 * b1 = f2 * b1 or f1 = f2 )
reconsider b = rng b1 as Basis of V1 by defOrdBasis;
assume A4:
f1 * b1 = f2 * b1
; f1 = f2
now for v being Element of V1 holds f1 . v = f2 . v
len b1 in Seg (len b1)
by A3, FINSEQ_1:3;
then reconsider D =
dom b1 as non
empty set by FINSEQ_1:def 3;
let v be
Element of
V1;
f1 . v = f2 . v
Lin b = ModuleStr(# the
carrier of
V1, the
addF of
V1, the
ZeroF of
V1, the
lmult of
V1 #)
by VECTSP_7:def 3;
then
v in Lin b
;
then consider KL being
Linear_Combination of
b such that A5:
v = Sum KL
by ZMODUL02:64;
set p =
KL (#) b1;
set A =
{ ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ;
A6:
rng (KL (#) b1) c= { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum }
A10:
for
w being
Element of
V1 st
w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } holds
f1 . w = f2 . w
A12:
(
b1 is
one-to-one &
Carrier KL c= rng b1 )
by defOrdBasis, VECTSP_6:def 4;
hence f1 . v =
f1 . (Sum (KL (#) b1))
by A5, Th20
.=
f2 . (Sum (KL (#) b1))
by A1, A2, A6, A10, Th21
.=
f2 . v
by A5, A12, Th20
;
verum end;
hence
f1 = f2
by FUNCT_2:63; verum