consider f being Function such that
A1: ( dom f = F₁() & ( for d being set st d in F₁() holds
f . d = F₂(d) ) ) from FUNCT_1:sch 3();
take f ; :: thesis: ( dom f = F₁() & ( for d being Element of F₁() holds f . d = F₂(d) ) )
thus dom f = F₁() by A1; :: thesis: for d being Element of F₁() holds f . d = F₂(d)
let d be Element of F₁(); :: thesis: f . d = F₂(d)
thus f . d = F₂(d) by A1; :: thesis: verum