let I be set ; :: thesis: for Y being non empty set

for x being b_{1} -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

for x being b

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