let o1, o2 be Function of (Funcs A,D1),(Funcs A,D2),(Funcs A,D); :: thesis: ( ( for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds o1 . f1,f2 = f .: f1,f2 ) & ( for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds o2 . f1,f2 = f .: f1,f2 ) implies o1 = o2 )
assume that
A2: for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds o1 . f1,f2 = f .: f1,f2 and
A3: for f1 being Element of Funcs A,D1
for f2 being Element of Funcs A,D2 holds o2 . f1,f2 = f .: f1,f2 ; :: thesis: o1 = o2

now

let f1 be Element of Funcs A,D1; :: thesis: for f2 being Element of Funcs A,D2 holds o1 . f1,f2 = o2 . f1,f2
let f2 be Element of Funcs A,D2; :: thesis: o1 . f1,f2 = o2 . f1,f2
thus o1 . f1,f2 = f .: f1,f2 by A2
.= o2 . f1,f2 by A3 ; :: thesis: verum

end;

hence o1 = o2 by BINOP_1:2; :: thesis: verum