let K be Field; :: thesis: for V1, V2 being finite-dimensional VectSp of K
for f1, f2 being Function of V1,V2
for A being set
for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds
f1 . v = f2 . v ) holds
f1 . (Sum p) = f2 . (Sum p)
let V1, V2 be finite-dimensional VectSp of K; :: thesis: for f1, f2 being Function of V1,V2
for A being set
for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds
f1 . v = f2 . v ) holds
f1 . (Sum p) = f2 . (Sum p)
let f1, f2 be Function of V1,V2; :: thesis: for A being set
for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds
f1 . v = f2 . v ) holds
f1 . (Sum p) = f2 . (Sum p)
let A be set ; :: thesis: for p being FinSequence of V1 st rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds
f1 . v = f2 . v ) holds
f1 . (Sum p) = f2 . (Sum p)
let p be FinSequence of V1; :: thesis: ( rng p c= A & f1 is additive & f1 is homogeneous & f2 is additive & f2 is homogeneous & ( for v being Element of V1 st v in A holds
f1 . v = f2 . v ) implies f1 . (Sum p) = f2 . (Sum p) )
assume A1: rng p c= A ; :: thesis: ( not f1 is additive or not f1 is homogeneous or not f2 is additive or not f2 is homogeneous or ex v being Element of V1 st
( v in A & not f1 . v = f2 . v ) or f1 . (Sum p) = f2 . (Sum p) )
defpred S1[ FinSequence of V1] means ( rng $1 c= A implies f1 . (Sum $1) = f2 . (Sum $1) );
assume A2: ( f1 is additive & f1 is homogeneous ) ; :: thesis: ( not f2 is additive or not f2 is homogeneous or ex v being Element of V1 st
( v in A & not f1 . v = f2 . v ) or f1 . (Sum p) = f2 . (Sum p) )
assume A3: ( f2 is additive & f2 is homogeneous ) ; :: thesis: ( ex v being Element of V1 st
( v in A & not f1 . v = f2 . v ) or f1 . (Sum p) = f2 . (Sum p) )
assume A4: for v being Element of V1 st v in A holds
f1 . v = f2 . v ; :: thesis: f1 . (Sum p) = f2 . (Sum p)
A5: for p being FinSequence of V1
for x being Element of V1 st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of V1; :: thesis: for x being Element of V1 st S1[p] holds
S1[p ^ <*x*>]
let x be Element of V1; :: thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A6: ( rng p c= A implies f1 . (Sum p) = f2 . (Sum p) ) ; :: thesis: S1[p ^ <*x*>]
A7: rng p c= (rng p) \/ (rng <*x*>) by XBOOLE_1:7;
assume rng (p ^ <*x*>) c= A ; :: thesis: f1 . (Sum (p ^ <*x*>)) = f2 . (Sum (p ^ <*x*>))
then A8: (rng p) \/ (rng <*x*>) c= A by FINSEQ_1:31;
rng <*x*> c= (rng p) \/ (rng <*x*>) by XBOOLE_1:7;
then rng <*x*> c= A by A8;
then {x} c= A by FINSEQ_1:39;
then A9: x in A by ZFMISC_1:31;
thus f1 . (Sum (p ^ <*x*>)) = f1 . ((Sum p) + (Sum <*x*>)) by RLVECT_1:41
.= (f2 . (Sum p)) + (f1 . (Sum <*x*>)) by A2, A6, A8, A7, VECTSP_1:def 20
.= (f2 . (Sum p)) + (f1 . x) by RLVECT_1:44
.= (f2 . (Sum p)) + (f2 . x) by A4, A9
.= (f2 . (Sum p)) + (f2 . (Sum <*x*>)) by RLVECT_1:44
.= f2 . ((Sum p) + (Sum <*x*>)) by A3, VECTSP_1:def 20
.= f2 . (Sum (p ^ <*x*>)) by RLVECT_1:41 ; :: thesis: verum
end;
A10: S1[ <*> the carrier of V1]
proof
assume rng (<*> the carrier of V1) c= A ; :: thesis: f1 . (Sum (<*> the carrier of V1)) = f2 . (Sum (<*> the carrier of V1))
thus f1 . (Sum (<*> the carrier of V1)) = f1 . (0. V1) by RLVECT_1:43
.= f1 . ((0. K) * (0. V1)) by VECTSP_1:14
.= (0. K) * (f1 . (0. V1)) by A2, MOD_2:def 2
.= 0. V2 by VECTSP_1:14
.= (0. K) * (f2 . (0. V1)) by VECTSP_1:14
.= f2 . ((0. K) * (0. V1)) by A3, MOD_2:def 2
.= f2 . (0. V1) by VECTSP_1:14
.= f2 . (Sum (<*> the carrier of V1)) by RLVECT_1:43 ; :: thesis: verum
end;
for p being FinSequence of V1 holds S1[p] from FINSEQ_2:sch 2(A10, A5);
 hence f1 . (Sum p) = f2 . (Sum p) by A1; :: thesis: verum