theorem :: FINSEQ_2:127

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