let I be non empty set ; :: thesis: for J being set
for A, B being ManySortedSet of I
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 I
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let A, B be ManySortedSet of I; :: 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 object st i in J holds
([|A,B|] * f) . i = [|(A * f),(B * f)|] . i

proof

A1: dom (B * f) = J by PARTFUN1:def 2;
let i be object ; :: thesis: ( i in J implies ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i )
A2: dom (A * f) = J by PARTFUN1:def 2;
assume A3: i in J ; :: thesis: ([|A,B|] * f) . i = [|(A * f),(B * f)|] . i
then A4: f . i in I by FUNCT_2:5;
dom ([|A,B|] * f) = J by PARTFUN1:def 2;
hence ([|A,B|] * f) . i = [|A,B|] . (f . i) by A3, FUNCT_1:12
.= [:(A . (f . i)),(B . (f . i)):] by A4, PBOOLE:def 16
.= [:((A * f) . i),(B . (f . i)):] by A3, A2, FUNCT_1:12
.= [:((A * f) . i),((B * f) . i):] by A3, A1, FUNCT_1:12
.= [|(A * f),(B * f)|] . i by A3, PBOOLE:def 16 ;
:: thesis: verum

end;

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