let I be set ; :: thesis: for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds
A is_transformable_to C
let A, B, C be ManySortedSet of I; :: thesis: ( A is_transformable_to B & B is_transformable_to C implies A is_transformable_to C )
assume that
A1: A is_transformable_to B and
A2: 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 A3: i in I ; :: thesis: ( not C . i = {} or A . i = {} )
then ( B . i = {} implies A . i = {} ) by A1;
hence ( not C . i = {} or A . i = {} ) by A2, A3; :: thesis: verum