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