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 :: thesis: for f1 being Element of Funcs (A,D1)
for f2 being Element of Funcs (A,D2) holds o1 . (f1,f2) = o2 . (f1,f2)

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 ; :: thesis: verum