let f, g be Function of [:A,B:],[:B,A:]; :: thesis: ( ( 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 )] ; :: thesis: f = g

now

let a be Element of [:A,B:]; :: thesis: f . a = g . a
f . a = [(a `2 ),(a `1 )] by A1;
hence f . a = g . a by A2; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum