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₁[ set , set ] 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

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

now

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

consider u being Element of Z;
u in Z ;
hence ex u being set 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 set 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 ) ) ;
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 set st e in Y holds
S₁[e,H . e] from FUNCT_2:sch 1(A2);
take H ; :: thesis: H * F = G

now

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

end;

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