let I, J, K be set ; :: thesis: for A being ManySortedSet of
for B being ManySortedSet of
for C being ManySortedSet of st A cc= B & B cc= C holds
A cc= C
let A be ManySortedSet of ; :: thesis: for B being ManySortedSet of
for C being ManySortedSet of st A cc= B & B cc= C holds
A cc= C
let B be ManySortedSet of ; :: thesis: for C being ManySortedSet of st A cc= B & B cc= C holds
A cc= C
let C be ManySortedSet of ; :: 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, Def2;
J c= K by A2, Def2;
hence I c= K by A3, XBOOLE_1:1; :: 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, Def2;
B . i c= C . i by A2, A3, A4, Def2;
hence A . i c= C . i by A5, XBOOLE_1:1; :: thesis: verum