let I be set ; 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; for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A
let F be ManySortedFunction of A,B; F "" C is ManySortedSubset of A
let i be object ; PBOOLE:def 2,PBOOLE:def 18 ( not i in I or (F "" C) . i c= A . i )
assume A1:
i in I
; (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; verum