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

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

hence
f = g
by FUNCT_2:63; :: thesis: verumlet 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;f . a = [(a `2),(a `1)] by A1;

hence f . a = g . a by A2; :: thesis: verum