let I be set ; :: thesis: for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A
let A, B, C be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A
let F be ManySortedFunction of A,B; :: thesis: F "" C is ManySortedSubset of A
let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not i in I or (F "" C) . i c= A . i )
assume A1: i in I ; :: thesis: (F "" C) . i c= A . i
then reconsider J = I as non empty set ;
reconsider j = i as Element of J by A1;
reconsider A1 = A, B1 = B as ManySortedSet of J ;
reconsider F1 = F as ManySortedFunction of A1,B1 ;
(F1 . j) " (C . j) c= A . j ;
hence (F "" C) . i c= A . i by Def1; :: thesis: verum