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 :: thesis: for a being Element of [:A,B:] holds f . a = g . a
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:63; :: thesis: verum