let I be set ; :: thesis: for A, X being ManySortedSet of
for B being V8() ManySortedSet of
for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let A, X be ManySortedSet of ; :: thesis: for B being V8() ManySortedSet of
for F being ManySortedFunction of A,B st X in A holds
F .. X in B
let B be V8() ManySortedSet of ; :: 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 set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or (F .. X) . i in B . i )
assume A2: i in I ; :: thesis: (F .. X) . i in B . i
A3: dom F = I by PARTFUN1:def 4;
reconsider g = F . i as Function ;
A4: g is Function of (A . i),(B . i) by A2, PBOOLE:def 18;
A5: B . i <> {} by A2;
X . i in A . i by A1, A2, PBOOLE:def 4;
then g . (X . i) in B . i by A4, A5, FUNCT_2:7;
hence (F .. X) . i in B . i by A2, A3, PRALG_1:def 17; :: thesis: verum