let Y, Z be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

proof

thus len q = len p by FINSEQ_2:33
.= len r by FINSEQ_2:33 ; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len q or q . b₁ = r . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len q or q . k = r . k )
assume that
A6: 1 <= k and
A7: k <= len q ; :: thesis: q . k = r . k
k <= len p by A7, FINSEQ_2:33;
then k in Seg (len p) by A6, FINSEQ_1:1;
then A8: k in dom p by FINSEQ_1:def 3;
hence q . k = f . (p . k) by FUNCT_1:13
.= g . (p . k) by A3, A8, FUNCT_1:3
.= r . k by FUNCT_1:13, A8 ;
:: thesis: verum

end;

hence f * p = g * p ; :: thesis: verum