theorem Th6: :: FINSEQOP:6

for X, x1, x2 being set holds <:(X --> x1),(X --> x2):> = X --> [x1,x2]