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 4;
hence ((X #) * f) . x = (X #) . p by A1, A2, FUNCT_1:22
.= product (X * p) by PBOOLE:def 19 ;
:: thesis: verum