let Y, Z be set ; for D being non empty set
for p being FinSequence
for f being Function of Y,D
for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds
f . a = g . a ) holds
f * p = g * p
let D be non empty set ; for p being FinSequence
for f being Function of Y,D
for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds
f . a = g . a ) holds
f * p = g * p
let p be FinSequence; for f being Function of Y,D
for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds
f . a = g . a ) holds
f * p = g * p
let f be Function of Y,D; for g being Function of Z,D st rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds
f . a = g . a ) holds
f * p = g * p
let g be Function of Z,D; ( rng p c= Y & rng p c= Z & ( for a being object st a in rng p holds
f . a = g . a ) implies f * p = g * p )
assume that
A1:
rng p c= Y
and
A2:
rng p c= Z
and
A3:
for a being object st a in rng p holds
f . a = g . a
; f * p = g * p
reconsider p1 = p as FinSequence of Y by A1, FINSEQ_1:def 4;
reconsider q = f * p1 as FinSequence by FINSEQ_2:32;
reconsider p2 = p as FinSequence of Z by A2, FINSEQ_1:def 4;
reconsider r = g * p2 as FinSequence by FINSEQ_2:32;
q = r
hence
f * p = g * p
; verum