let f be Function; for A being set
for a, b being object st a in A & b in A holds
(f || A) . (a,b) = f . (a,b)
let A be set ; for a, b being object st a in A & b in A holds
(f || A) . (a,b) = f . (a,b)
let a, b be object ; ( a in A & b in A implies (f || A) . (a,b) = f . (a,b) )
assume
( a in A & b in A )
; (f || A) . (a,b) = f . (a,b)
then
[a,b] in [:A,A:]
by ZFMISC_1:def 2;
hence
(f || A) . (a,b) = f . (a,b)
by FUNCT_1:49; verum