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 S_{1}[ 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_{1}[p] holds

S_{1}[p ^ <*x*>]
_{1}[ <*> the carrier of V1]
_{1}[p]
from FINSEQ_2:sch 2(A10, A5);

hence f1 . (Sum p) = f2 . (Sum p) by A1; :: thesis: verum

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 S

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

S

proof

A10:
S
let p be FinSequence of V1; :: thesis: for x being Element of V1 st S_{1}[p] holds

S_{1}[p ^ <*x*>]

let x be Element of V1; :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*x*>] )

assume A6: ( rng p c= A implies f1 . (Sum p) = f2 . (Sum p) ) ; :: thesis: S_{1}[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;S

let x be Element of V1; :: thesis: ( S

assume A6: ( rng p c= A implies f1 . (Sum p) = f2 . (Sum p) ) ; :: thesis: S

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

proof

for p being FinSequence of V1 holds S
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;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

hence f1 . (Sum p) = f2 . (Sum p) by A1; :: thesis: verum