:: deftheorem defines (1,2)->(1,?,2) COMPUT_1:def 22 :
for g being Function holds (1,2)->(1,?,2) g = g * <:<*(3 proj 1),(3 proj 3)*>:>;