let I be set ; :: thesis: for A, X being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let A, X be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let F be ManySortedFunction of A,B; :: thesis: ( X in A implies F .. X in B )
assume A1: X in A ; :: thesis: F .. X in B
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or (F .. X) . i in B . i )
assume A2: i in I ; :: thesis: (F .. X) . i in B . i
reconsider g = F . i as Function ;
A3: g is Function of (A . i),(B . i) by A2, PBOOLE:def 15;
X . i in A . i by A1, A2;
then ( dom F = I & g . (X . i) in B . i ) by A2, A3, FUNCT_2:5, PARTFUN1:def 2;
hence (F .. X) . i in B . i by A2, PRALG_1:def 20; :: thesis: verum