let K be Field; :: thesis: for V2, V1 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 V2, V1 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 S₁[ 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 S₁[p] holds
S₁[p ^ <*x*>]

proof

let p be FinSequence of V1; :: thesis: for x being Element of V1 st S₁[p] holds
S₁[p ^ <*x*>]
let x be Element of V1; :: thesis: ( S₁[p] implies S₁[p ^ <*x*>] )
assume A6: ( rng p c= A implies f1 . (Sum p) = f2 . (Sum p) ) ; :: thesis: S₁[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:44;
rng <*x*> c= (rng p) \/ (rng <*x*>) by XBOOLE_1:7;
then rng <*x*> c= A by A8, XBOOLE_1:1;
then {x} c= A by FINSEQ_1:56;
then A9: x in A by ZFMISC_1:37;
thus f1 . (Sum (p ^ <*x*>)) = f1 . ((Sum p) + (Sum <*x*>)) by RLVECT_1:58
.= (f2 . (Sum p)) + (f1 . (Sum <*x*>)) by A2, A6, A8, A7, MOD_2:def 3, GRCAT_1:def 13, XBOOLE_1:1
.= (f2 . (Sum p)) + (f1 . x) by RLVECT_1:61
.= (f2 . (Sum p)) + (f2 . x) by A4, A9
.= (f2 . (Sum p)) + (f2 . (Sum <*x*>)) by RLVECT_1:61
.= f2 . ((Sum p) + (Sum <*x*>)) by A3, MOD_2:def 3, GRCAT_1:def 13
.= f2 . (Sum (p ^ <*x*>)) by RLVECT_1:58 ; :: thesis: verum

end;

A10: S₁[ <*> 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:60
.= f1 . ((0. K) * (0. V1)) by VECTSP_1:59
.= (0. K) * (f1 . (0. V1)) by A2, MOD_2:def 3, GRCAT_1:def 13
.= 0. V2 by VECTSP_1:59
.= (0. K) * (f2 . (0. V1)) by VECTSP_1:59
.= f2 . ((0. K) * (0. V1)) by A3, MOD_2:def 3, GRCAT_1:def 13
.= f2 . (0. V1) by VECTSP_1:59
.= f2 . (Sum (<*> the carrier of V1)) by RLVECT_1:60 ; :: thesis: verum

end;

for p being FinSequence of V1 holds S₁[p] from FINSEQ_2:sch 2(A10, A5);
hence f1 . (Sum p) = f2 . (Sum p) by A1; :: thesis: verum