deffunc H1( Element of 3 -tuples_on F1()) -> Element of F1() = F2(($1 . 1),($1 . 2),($1 . 3));
consider f being Function of (3 -tuples_on F1()),F1() such that
A1:
for a being Element of 3 -tuples_on F1() holds f . a = H1(a)
from FUNCT_2:sch 4();
hereby for f1, f2 being Function of (3 -tuples_on F1()),F1() st ( for x, y, z being Element of F1() holds f1 . <*x,y,z*> = F2(x,y,z) ) & ( for x, y, z being Element of F1() holds f2 . <*x,y,z*> = F2(x,y,z) ) holds
f1 = f2
take f =
f;
for x, y, z being Element of F1() holds f . <*x,y,z*> = F2(x,y,z)let x,
y,
z be
Element of
F1();
f . <*x,y,z*> = F2(x,y,z)reconsider a =
<*x,y,z*> as
Element of 3
-tuples_on F1()
by FINSEQ_2:104;
thus f . <*x,y,z*> =
F2(
(a . 1),
(a . 2),
(a . 3))
by A1
.=
F2(
x,
(a . 2),
(a . 3))
by FINSEQ_1:45
.=
F2(
x,
y,
(a . 3))
by FINSEQ_1:45
.=
F2(
x,
y,
z)
by FINSEQ_1:45
;
verum
end;
let f1, f2 be Function of (3 -tuples_on F1()),F1(); ( ( for x, y, z being Element of F1() holds f1 . <*x,y,z*> = F2(x,y,z) ) & ( for x, y, z being Element of F1() holds f2 . <*x,y,z*> = F2(x,y,z) ) implies f1 = f2 )
assume that
A2:
for x, y, z being Element of F1() holds f1 . <*x,y,z*> = F2(x,y,z)
and
A3:
for x, y, z being Element of F1() holds f2 . <*x,y,z*> = F2(x,y,z)
; f1 = f2
hence
f1 = f2
by FUNCT_2:63; verum