let I be non empty set ; 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 ; 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; for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]
let f be Function of J,I; [|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 ;
( 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
;
([|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
;
verum
end;
hence
[|A,B|] * f = [|(A * f),(B * f)|]
; verum