let X, Y, Z be non empty set ; :: thesis: for F being Function of X,Y

for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ) holds

ex H being Function of Y,Z st H * F = G

let F be Function of X,Y; :: thesis: for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ) holds

ex H being Function of Y,Z st H * F = G

let G be Function of X,Z; :: thesis: ( ( for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ) implies ex H being Function of Y,Z st H * F = G )

defpred S_{1}[ object , object ] means ( for x being Element of X holds not $1 = F . x or for x being Element of X st $1 = F . x holds

$2 = G . x );

assume A1: for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ; :: thesis: ex H being Function of Y,Z st H * F = G

A7: for e being object st e in Y holds

S_{1}[e,H . e]
from FUNCT_2:sch 1(A2);

take H ; :: thesis: H * F = G

for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ) holds

ex H being Function of Y,Z st H * F = G

let F be Function of X,Y; :: thesis: for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ) holds

ex H being Function of Y,Z st H * F = G

let G be Function of X,Z; :: thesis: ( ( for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ) implies ex H being Function of Y,Z st H * F = G )

defpred S

$2 = G . x );

assume A1: for x, x9 being Element of X st F . x = F . x9 holds

G . x = G . x9 ; :: thesis: ex H being Function of Y,Z st H * F = G

A2: now :: thesis: for e being object st e in Y holds

ex u being object st

( u in Z & S_{1}[e,u] )

consider H being Function of Y,Z such that ex u being object st

( u in Z & S

let e be object ; :: thesis: ( e in Y implies ex u being object st

( u in Z & S_{1}[e,u] ) )

assume e in Y ; :: thesis: ex u being object st

( u in Z & S_{1}[e,u] )

A5: u in Z and

A6: ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ;

reconsider u = u as object ;

take u = u; :: thesis: ( u in Z & S_{1}[e,u] )

thus u in Z by A5; :: thesis: S_{1}[e,u]

thus S_{1}[e,u]
by A1, A6; :: thesis: verum

end;( u in Z & S

assume e in Y ; :: thesis: ex u being object st

( u in Z & S

now :: thesis: ( ( ex x being Element of X st e = F . x & ex u being Element of Z st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) ) or ( ( for x being Element of X holds not e = F . x ) & ex u being object st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) ) )end;

then consider u being object such that ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) ) or ( ( for x being Element of X holds not e = F . x ) & ex u being object st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) ) )

per cases
( ex x being Element of X st e = F . x or for x being Element of X holds not e = F . x )
;

end;

case
ex x being Element of X st e = F . x
; :: thesis: ex u being Element of Z st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) )

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) )

then consider x being Element of X such that

A3: e = F . x ;

take u = G . x; :: thesis: ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) )

thus ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) by A3; :: thesis: verum

end;A3: e = F . x ;

take u = G . x; :: thesis: ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) )

thus ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) by A3; :: thesis: verum

case A4:
for x being Element of X holds not e = F . x
; :: thesis: ex u being object st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) )

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) )

set u = the Element of Z;

the Element of Z in Z ;

hence ex u being object st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) by A4; :: thesis: verum

end;the Element of Z in Z ;

hence ex u being object st

( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ) by A4; :: thesis: verum

A5: u in Z and

A6: ( ex x being Element of X st e = F . x implies ex x being Element of X st

( e = F . x & u = G . x ) ) ;

reconsider u = u as object ;

take u = u; :: thesis: ( u in Z & S

thus u in Z by A5; :: thesis: S

thus S

A7: for e being object st e in Y holds

S

take H ; :: thesis: H * F = G

now :: thesis: for x being Element of X holds (H * F) . x = G . x

hence
H * F = G
by FUNCT_2:63; :: thesis: verumlet x be Element of X; :: thesis: (H * F) . x = G . x

thus (H * F) . x = H . (F . x) by FUNCT_2:15

.= G . x by A7 ; :: thesis: verum

end;thus (H * F) . x = H . (F . x) by FUNCT_2:15

.= G . x by A7 ; :: thesis: verum