let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
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 V1, V2 be finite-dimensional VectSp of K; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: for b1 being OrdBasis of V1 st len b1 > 0 & f1 * b1 = f2 * b1 holds
f1 = f2
let b1 be OrdBasis of V1; :: thesis: ( len b1 > 0 & f1 * b1 = f2 * b1 implies f1 = f2 )
assume A3: len b1 > 0 ; :: thesis: ( not f1 * b1 = f2 * b1 or f1 = f2 )
reconsider b = rng b1 as Basis of V1 by Def2;
assume A4: f1 * b1 = f2 * b1 ; :: thesis: f1 = f2
now :: thesis: 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; :: thesis: 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 by RLVECT_1:1;
then consider KL being Linear_Combination of b such that
A5: v = Sum KL by VECTSP_7:7;
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 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (KL (#) b1) or x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } )
assume x in rng (KL (#) b1) ; :: thesis: x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum }
then consider i being Nat such that
A7: i in dom (KL (#) b1) and
A8: (KL (#) b1) . i = x by FINSEQ_2:10;
dom (KL (#) b1) = Seg (len (KL (#) b1)) by FINSEQ_1:def 3;
then i in Seg (len b1) by A7, VECTSP_6:def 5;
then A9: i in dom b1 by FINSEQ_1:def 3;
(KL (#) b1) . i = (KL . (b1 /. i)) * (b1 /. i) by A7, VECTSP_6:def 5;
hence x in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } by A8, A9; :: thesis: verum
end;
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
proof
let w be Element of V1; :: thesis: ( w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } implies f1 . w = f2 . w )
assume w in { ((KL . (b1 /. i)) * (b1 /. i)) where i is Element of D : verum } ; :: thesis: f1 . w = f2 . w
then consider i being Element of D such that
A11: w = (KL . (b1 /. i)) * (b1 /. i) ;
f1 . (b1 /. i) = f1 . (b1 . i) by PARTFUN1:def 6
.= (f2 * b1) . i by A4, FUNCT_1:13
.= f2 . (b1 . i) by FUNCT_1:13
.= f2 . (b1 /. i) by PARTFUN1:def 6 ;
then f1 . ((KL . (b1 /. i)) * (b1 /. i)) = (KL . (b1 /. i)) * (f2 . (b1 /. i)) by A1, MOD_2:def 2
.= f2 . ((KL . (b1 /. i)) * (b1 /. i)) by A2, MOD_2:def 2 ;
hence f1 . w = f2 . w by A11; :: thesis: verum
end;
A12: ( b1 is one-to-one & Carrier KL c= rng b1 ) by Def2, 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 ;
:: thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; :: thesis: verum