let I be set ; :: thesis: for Y being non empty set
for x being b₁ -valued ManySortedSet of I
for p being FinSequence of I holds p * x is FinSequence of Y
let Y be non empty set ; :: thesis: for x being Y -valued ManySortedSet of I
for p being FinSequence of I holds p * x is FinSequence of Y
let x be Y -valued ManySortedSet of I; :: thesis: for p being FinSequence of I holds p * x is FinSequence of Y
let p be FinSequence of I; :: thesis: p * x is FinSequence of Y
A1: dom x = I by PARTFUN1:def 2;
A2: rng x c= Y by RELAT_1:def 19;
then A3: x is Function of I,Y by A1, FUNCT_2:2;
reconsider x1 = x as Function of I,Y by A1, A2, FUNCT_2:2;
reconsider xp = p * x1 as FinSequence ;
thus p * x is FinSequence of Y by A3, FINSEQ_2:32; :: thesis: verum