let I be set ; :: thesis: for A, B being ManySortedSet of st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for C being ManySortedSet of st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
let A, B be ManySortedSet of ; :: thesis: ( A is_transformable_to B implies for F being ManySortedFunction of A,B
for C being ManySortedSet of 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 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 st B is ManySortedSubset of C holds
F is ManySortedFunction of A,C
let C be ManySortedSet of ; :: 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 Element of K21(K22((A . i),(C . i))) )
assume A3: i in I ; :: thesis: F . i is Element of K21(K22((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 Element of K21(K22((A . i),(C . i))) by A4, A5, FUNCT_2:9; :: thesis: verum