let V1, V2 be free finite-rank Z_Module; :: 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 that
A2: ( f1 is additive & f1 is homogeneous ) and
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:31;
rng <*x*> c= (rng p) \/ (rng <*x*>) by XBOOLE_1:7;
then rng <*x*> c= A by A8;
then A9: {x} c= A by FINSEQ_1:39;
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
.= (f2 . (Sum p)) + (f1 . x) by RLVECT_1:44
.= (f2 . (Sum p)) + (f2 . x) by A4, A9, ZFMISC_1:31
.= (f2 . (Sum p)) + (f2 . (Sum <*x*>)) by RLVECT_1:44
.= f2 . ((Sum p) + (Sum <*x*>)) by A3
.= f2 . (Sum (p ^ <*x*>)) by RLVECT_1:41 ; :: 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))
set I0 = 0. INT.Ring;
thus f1 . (Sum (<*> the carrier of V1)) = f1 . (0. V1) by RLVECT_1:43
.= f1 . ((0. INT.Ring) * (0. V1)) by ZMODUL01:1
.= (0. INT.Ring) * (f1 . (0. V1)) by A2
.= 0. V2 by ZMODUL01:1
.= (0. INT.Ring) * (f2 . (0. V1)) by ZMODUL01:1
.= f2 . ((0. INT.Ring) * (0. V1)) by A3
.= f2 . (0. V1) by ZMODUL01:1
.= f2 . (Sum (<*> the carrier of V1)) by RLVECT_1:43 ; :: 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