let f1, f2 be Element of Funcs F₁(),BOOLEAN ; :: thesis: ( ( for x being Element of F₁() holds f1 . x = F₂(x) ) & ( for x being Element of F₁() holds f2 . x = F₂(x) ) implies f1 = f2 )
assume that
A1: for x being Element of F₁() holds f1 . x = F₂(x) and
A2: for x being Element of F₁() holds f2 . x = F₂(x) ; :: thesis: f1 = f2
consider k3 being Function such that
A3: ( f1 = k3 & dom k3 = F₁() & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A4: ( f2 = k4 & dom k4 = F₁() & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in F₁() holds
k3 . u = k4 . u

proof

let u be set ; :: thesis: ( u in F₁() implies k3 . u = k4 . u )
assume u in F₁() ; :: thesis: k3 . u = k4 . u
then reconsider u' = u as Element of F₁() ;
f2 . u' = F₂(u') by A2;
hence k3 . u = k4 . u by A1, A3, A4; :: thesis: verum

end;

hence f1 = f2 by A3, A4, FUNCT_1:9; :: thesis: verum