let x, y be object ; :: thesis: for f, g being Function holds (Ext (f,x,y)) * g = Ext ((f * g),x,y)
let f, g be Function; :: thesis: (Ext (f,x,y)) * g = Ext ((f * g),x,y)
set E = Ext (f,x,y);
set Eg = Ext ((f * g),x,y);
A1: ( dom (Ext (f,x,y)) = dom f & dom (Ext ((f * g),x,y)) = dom (f * g) ) by Def5;
A2: dom ((Ext (f,x,y)) * g) c= dom (f * g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom ((Ext (f,x,y)) * g) or a in dom (f * g) )
assume a in dom ((Ext (f,x,y)) * g) ; :: thesis: a in dom (f * g)
then ( a in dom g & g . a in dom (Ext (f,x,y)) ) by FUNCT_1:11;
hence a in dom (f * g) by A1, FUNCT_1:11; :: thesis: verum

end;

dom (f * g) c= dom ((Ext (f,x,y)) * g)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom (f * g) or a in dom ((Ext (f,x,y)) * g) )
assume a in dom (f * g) ; :: thesis: a in dom ((Ext (f,x,y)) * g)
then ( a in dom g & g . a in dom f ) by FUNCT_1:11;
hence a in dom ((Ext (f,x,y)) * g) by A1, FUNCT_1:11; :: thesis: verum

end;

then A3: dom (Ext ((f * g),x,y)) = dom ((Ext (f,x,y)) * g) by A2, Def5;
for a being object st a in dom (Ext ((f * g),x,y)) holds
(Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a

proof

let a be object ; :: thesis: ( a in dom (Ext ((f * g),x,y)) implies (Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a )
assume A4: a in dom (Ext ((f * g),x,y)) ; :: thesis: (Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a
A5: a in dom (f * g) by A4, Def5;
then A6: (f * g) . a = f . (g . a) by FUNCT_1:12;
A7: ( ((Ext (f,x,y)) * g) . a = (Ext (f,x,y)) . (g . a) & g . a in dom (Ext (f,x,y)) ) by A4, A3, FUNCT_1:11, FUNCT_1:12;

per cases ( x in (f * g) . a or not x in (f * g) . a ) ;

suppose A8: x in (f * g) . a ; :: thesis: (Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a

then (Ext ((f * g),x,y)) . a = ((f * g) . a) \/ {y} by A5, Def5;
hence (Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a by A8, A6, A7, A1, Def5; :: thesis: verum

end;

suppose A9: not x in (f * g) . a ; :: thesis: (Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a

then (Ext ((f * g),x,y)) . a = (f * g) . a by A5, Def5;
hence (Ext ((f * g),x,y)) . a = ((Ext (f,x,y)) * g) . a by A9, A6, A7, A1, Def5; :: thesis: verum

end;

end;

end;

hence (Ext (f,x,y)) * g = Ext ((f * g),x,y) by A3; :: thesis: verum