let f, g be Function of [:A,B:],[:B,A:]; ( ( for a being Element of [:A,B:] holds f . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds g . a = [(a `2),(a `1)] ) implies f = g )
assume that
A1:
for a being Element of [:A,B:] holds f . a = [(a `2),(a `1)]
and
A2:
for a being Element of [:A,B:] holds g . a = [(a `2),(a `1)]
; f = g
hence
f = g
by FUNCT_2:63; verum