theorem :: YELLOW10:36

for S, T being non empty RelStr
for s being Element of S
for t being Element of T holds [:(downarrow s),(downarrow t):] = downarrow [s,t]