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 A2: B is ManySortedSubset of C ; :: thesis: F is ManySortedFunction of A,C
let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in I or F . i is Relation of A . i,C . i )
assume A3: i in I ; :: thesis: F . i is Relation of A . i,C . i
B c= C by A2, PBOOLE:def 23;
then A4: B . i c= C . i by A3, PBOOLE:def 5;
A5: ( B . i = {} implies A . i = {} ) by A1, A3, PZFMISC1:def 3;
F . i is Function of A . i,B . i by A3, PBOOLE:def 18;
hence F . i is Function of A . i,C . i by A4, A5, FUNCT_2:9; :: thesis: verum