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₁[ 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

A2: now :: thesis: for e being object st e in Y holds
ex u being object st
( u in Z & S₁[e,u] )

let e be object ; :: thesis: ( e in Y implies ex u being object st
( u in Z & S₁[e,u] ) )
assume e in Y ; :: thesis: ex u being object st
( u in Z & S₁[e,u] )

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 ) ) ) ) )

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

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 ) ) )

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;

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 ) ) )

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;

end;

end;

then consider u being object such that
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₁[e,u] )
thus u in Z by A5; :: thesis: S₁[e,u]
thus S₁[e,u] by A1, A6; :: thesis: verum

end;

consider H being Function of Y,Z such that
A7: for e being object st e in Y holds
S₁[e,H . e] from FUNCT_2:sch 1(A2);
take H ; :: thesis: H * F = G

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

let 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;

hence H * F = G by FUNCT_2:63; :: thesis: verum