defpred S1[ Element of F1(), set ] means ( ( $1 = F3() implies $2 = F6() ) & ( $1 = F4() implies $2 = F7() ) & ( $1 = F5() implies $2 = F8() ) & ( $1 <> F3() & $1 <> F4() & $1 <> F5() implies $2 = F9($1) ) );
A4:
for x being Element of F1() ex y being Element of F2() st S1[x,y]
proof
let x be
Element of
F1();
ex y being Element of F2() st S1[x,y]
A5:
(
x = F4() implies ex
y being
Element of
F2() st
S1[
x,
y] )
by A1, A3;
A6:
(
x = F5() implies ex
y being
Element of
F2() st
S1[
x,
y] )
by A2, A3;
(
x = F3() implies ex
y being
Element of
F2() st
S1[
x,
y] )
by A1, A2;
hence
ex
y being
Element of
F2() st
S1[
x,
y]
by A5, A6;
verum
end;
consider f being Function of F1(),F2() such that
A7:
for x being Element of F1() holds S1[x,f . x]
from FUNCT_2:sch 3(A4);
take
f
; ( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds
f . C = F9(C) ) )
thus
( f . F3() = F6() & f . F4() = F7() & f . F5() = F8() & ( for C being Element of F1() st C <> F3() & C <> F4() & C <> F5() holds
f . C = F9(C) ) )
by A7; verum