let I, J, K be set ; :: thesis: for A being ManySortedSet of I

for B being ManySortedSet of J

for C being ManySortedSet of K st A cc= B & B cc= C holds

A cc= C

let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J

for C being ManySortedSet of K st A cc= B & B cc= C holds

A cc= C

let B be ManySortedSet of J; :: thesis: for C being ManySortedSet of K st A cc= B & B cc= C holds

A cc= C

let C be ManySortedSet of K; :: thesis: ( A cc= B & B cc= C implies A cc= C )

assume that

A1: A cc= B and

A2: B cc= C ; :: thesis: A cc= C

A3: I c= J by A1;

J c= K by A2;

hence I c= K by A3; :: according to ALTCAT_2:def 2 :: thesis: for i being set st i in I holds

A . i c= C . i

let i be set ; :: thesis: ( i in I implies A . i c= C . i )

assume A4: i in I ; :: thesis: A . i c= C . i

then A5: A . i c= B . i by A1;

B . i c= C . i by A2, A3, A4;

hence A . i c= C . i by A5; :: thesis: verum

for B being ManySortedSet of J

for C being ManySortedSet of K st A cc= B & B cc= C holds

A cc= C

let A be ManySortedSet of I; :: thesis: for B being ManySortedSet of J

for C being ManySortedSet of K st A cc= B & B cc= C holds

A cc= C

let B be ManySortedSet of J; :: thesis: for C being ManySortedSet of K st A cc= B & B cc= C holds

A cc= C

let C be ManySortedSet of K; :: thesis: ( A cc= B & B cc= C implies A cc= C )

assume that

A1: A cc= B and

A2: B cc= C ; :: thesis: A cc= C

A3: I c= J by A1;

J c= K by A2;

hence I c= K by A3; :: according to ALTCAT_2:def 2 :: thesis: for i being set st i in I holds

A . i c= C . i

let i be set ; :: thesis: ( i in I implies A . i c= C . i )

assume A4: i in I ; :: thesis: A . i c= C . i

then A5: A . i c= B . i by A1;

B . i c= C . i by A2, A3, A4;

hence A . i c= C . i by A5; :: thesis: verum