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