let f1, f2 be Element of Funcs (F1(),BOOLEAN); ( ( for x being Element of F1() holds f1 . x = F2(x) ) & ( for x being Element of F1() holds f2 . x = F2(x) ) implies f1 = f2 )
assume that
A1:
for x being Element of F1() holds f1 . x = F2(x)
and
A2:
for x being Element of F1() holds f2 . x = F2(x)
; f1 = f2
consider k3 being Function such that
A3:
f1 = k3
and
A4:
dom k3 = F1()
and
rng k3 c= BOOLEAN
by FUNCT_2:def 2;
consider k4 being Function such that
A5:
f2 = k4
and
A6:
dom k4 = F1()
and
rng k4 c= BOOLEAN
by FUNCT_2:def 2;
for u being set st u in F1() holds
k3 . u = k4 . u
proof
let u be
set ;
( u in F1() implies k3 . u = k4 . u )
assume
u in F1()
;
k3 . u = k4 . u
then reconsider u9 =
u as
Element of
F1() ;
f2 . u9 = F2(
u9)
by A2;
hence
k3 . u = k4 . u
by A1, A3, A5;
verum
end;
hence
f1 = f2
by A3, A4, A5, A6, FUNCT_1:2; verum