let I be non empty set ; :: thesis: for J being set
for A, B being ManySortedSet of
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let J be set ; :: thesis: for A, B being ManySortedSet of
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let A, B be ManySortedSet of ; :: thesis: for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let f be Function of J,I; :: thesis: [|A,B|] * f = [|(A * f),(B * f)|]
for i being set st i in J holds
([|A,B|] * f) . i = [|(A * f),(B * f)|] . i

proof

let i be set ; :: thesis: ( i in J implies ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i )
assume A1: i in J ; :: thesis: ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i
then A2: f . i in I by FUNCT_2:7;
A3: ( dom ([|A,B|] * f) = J & dom (A * f) = J & dom (B * f) = J ) by PARTFUN1:def 4;
hence ([|A,B|] * f) . i = [|A,B|] . (f . i) by A1, FUNCT_1:22
.= [:(A . (f . i)),(B . (f . i)):] by A2, PBOOLE:def 21
.= [:((A * f) . i),(B . (f . i)):] by A1, A3, FUNCT_1:22
.= [:((A * f) . i),((B * f) . i):] by A1, A3, FUNCT_1:22
.= [|(A * f),(B * f)|] . i by A1, PBOOLE:def 21 ;
:: thesis: verum

end;

hence [|A,B|] * f = [|(A * f),(B * f)|] by PBOOLE:3; :: thesis: verum