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

for f being Function of I,(J *)

for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let J be non empty set ; :: thesis: for f being Function of I,(J *)

for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let f be Function of I,(J *); :: thesis: for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let X be ManySortedSet of J; :: thesis: for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let p be Element of J * ; :: thesis: for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let x be set ; :: thesis: ( x in I & p = f . x implies ((X #) * f) . x = product (X * p) )

assume A1: ( x in I & p = f . x ) ; :: thesis: ((X #) * f) . x = product (X * p)

A2: dom f = I by FUNCT_2:def 1;

then dom ((X #) * f) = dom f by PARTFUN1:def 2;

hence ((X #) * f) . x = (X #) . p by A1, A2, FUNCT_1:12

.= product (X * p) by FINSEQ_2:def 5 ;

:: thesis: verum

for f being Function of I,(J *)

for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let J be non empty set ; :: thesis: for f being Function of I,(J *)

for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let f be Function of I,(J *); :: thesis: for X being ManySortedSet of J

for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let X be ManySortedSet of J; :: thesis: for p being Element of J *

for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let p be Element of J * ; :: thesis: for x being set st x in I & p = f . x holds

((X #) * f) . x = product (X * p)

let x be set ; :: thesis: ( x in I & p = f . x implies ((X #) * f) . x = product (X * p) )

assume A1: ( x in I & p = f . x ) ; :: thesis: ((X #) * f) . x = product (X * p)

A2: dom f = I by FUNCT_2:def 1;

then dom ((X #) * f) = dom f by PARTFUN1:def 2;

hence ((X #) * f) . x = (X #) . p by A1, A2, FUNCT_1:12

.= product (X * p) by FINSEQ_2:def 5 ;

:: thesis: verum