let I be set ; :: thesis: for A, B, C being ManySortedSet of st A is_transformable_to B & B is_transformable_to C holds
A is_transformable_to C
let A, B, C be ManySortedSet of ; :: thesis: ( A is_transformable_to B & B is_transformable_to C implies A is_transformable_to C )
assume A1: ( A is_transformable_to B & B is_transformable_to C ) ; :: thesis: A is_transformable_to C
let i be set ; :: according to PZFMISC1:def 3 :: thesis: ( not i in I or not C . i = {} or A . i = {} )
assume i in I ; :: thesis: ( not C . i = {} or A . i = {} )
then ( ( B . i = {} implies A . i = {} ) & ( C . i = {} implies B . i = {} ) ) by A1, PZFMISC1:def 3;
hence ( not C . i = {} or A . i = {} ) ; :: thesis: verum