let X, Y, Z be non empty set ; :: thesis:
let F be Function of X,Y; :: thesis:
let G be Function of X,Z; :: thesis:
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:

A2: now :: thesis:

let e be object ; :: thesis:
assume e in Y ; :: thesis:

now :: thesis:

per cases ;

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

then consider x being Element of X such that
A3: e = F . x ;
take u = G . x; :: thesis:
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:

end;

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

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:

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:
thus u in Z by A5; :: thesis:
thus S₁[e,u] by A1, A6; :: thesis:

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:

now :: thesis:

let x be Element of X; :: thesis:
thus (H * F) . x = H . (F . x) by FUNCT_2:15
.= G . x by A7 ; :: thesis:

end;

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