let f be Function; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( a in A & b in A implies (f || A) . (a,b) = f . (a,b) )
assume ( a in A & b in A ) ; :: thesis: (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; :: thesis: verum