let I be set ; :: thesis: for A, B being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
let A, B be ManySortedSet of I; :: thesis: ( A is_transformable_to B implies for F being ManySortedFunction of A,B
for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C )
assume A1: A is_transformable_to B ; :: thesis: for F being ManySortedFunction of A,B
for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
let F be ManySortedFunction of A,B; :: thesis: for C being ManySortedSet of I st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
let C be ManySortedSet of I; :: thesis: ( B is ManySortedSubset of C implies F is ManySortedFunction of A,C )
assume B is ManySortedSubset of C ; :: thesis: F is ManySortedFunction of A,C
then A2: B c= C by PBOOLE:def 18;
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I or F . i is Element of K19(K20((A . i),(C . i))) )
assume A3: i in I ; :: thesis: F . i is Element of K19(K20((A . i),(C . i)))
A4: ( B . i = {} implies A . i = {} ) by A1, A3, PZFMISC1:def 3;
A5: F . i is Function of (A . i),(B . i) by A3, PBOOLE:def 15;
B . i c= C . i by A3, A2;
hence F . i is Element of K19(K20((A . i),(C . i))) by A4, A5, FUNCT_2:7; :: thesis: verum