A1: dom f1 = A1 by Def1;
hence ( f1 = f2 implies ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) ) ) by Def1; :: thesis: ( A1 = A2 & ( for a being Element of A1 holds f1 . a = f2 . a ) implies f1 = f2 )
assume that
A2: A1 = A2 and
A3: for a being Element of A1 holds f1 . a = f2 . a ; :: thesis: f1 = f2
A4: dom f2 = A2 by Def1;
for a being object st a in A1 holds
f1 . a = f2 . a by A3;
hence f1 = f2 by A1, A4, A2; :: thesis: verum