let I be set ; :: thesis: for A, B being ManySortedSet of
for M being ManySortedSubset of A
for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A
let A, B be ManySortedSet of ; :: thesis: for M being ManySortedSubset of A
for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A
let M be ManySortedSubset of A; :: thesis: for F being ManySortedFunction of A,B holds F .:.: M c= F .:.: A
let F be ManySortedFunction of A,B; :: thesis: F .:.: M c= F .:.: A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (F .:.: M) . i c= (F .:.: A) . i )
assume A1: i in I ; :: thesis: (F .:.: M) . i c= (F .:.: A) . i
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (F .:.: M) . i or x in (F .:.: A) . i )
assume A2: x in (F .:.: M) . i ; :: thesis: x in (F .:.: A) . i
reconsider f = F . i as Function of (A . i),(B . i) by A1, PBOOLE:def 18;
A3: (F .:.: M) . i = f .: (M . i) by A1, PBOOLE:def 25;
M c= A by PBOOLE:def 23;
then M . i c= A . i by A1, PBOOLE:def 5;
then f .: (M . i) c= f .: (A . i) by RELAT_1:156;
then x in f .: (A . i) by A2, A3;
hence x in (F .:.: A) . i by A1, PBOOLE:def 25; :: thesis: verum