theorem Th21: :: AOFA_A00:26

for a1, a2, a3, a4, a5, a6, a7, a8, a9 being object holds rng (<*a1,a2,a3,a4,a5,a6,a7,a8*> ^ <*a9*>) = {a1,a2,a3,a4,a5,a6,a7,a8,a9}