theorem :: FINSEQ_2:128

for x1, x2, x3 being object holds rng <*x1,x2,x3*> = {x1,x2,x3} by Lm2;