defpred S₁[ object , object , object ] means for l2, l1 being Element of MapsC X st l2 = $1 & l1 = $2 holds
( dom l2 = cod l1 & $3 = l2 * l1 );
A5: for x, y, z1, z2 being object st x in MapsC X & y in MapsC X & S₁[x,y,z1] & S₁[x,y,z2] holds
z1 = z2

proof

let x, y, z1, z2 be object ; :: thesis: ( x in MapsC X & y in MapsC X & S₁[x,y,z1] & S₁[x,y,z2] implies z1 = z2 )
assume ( x in MapsC X & y in MapsC X ) ; :: thesis: ( not S₁[x,y,z1] or not S₁[x,y,z2] or z1 = z2 )
then reconsider l2 = x, l1 = y as Element of MapsC X ;
assume that
A6: S₁[x,y,z1] and
A7: S₁[x,y,z2] ; :: thesis: z1 = z2
z1 = l2 * l1 by A6;
hence z1 = z2 by A7; :: thesis: verum

end;

A8: for x, y, z being object st x in MapsC X & y in MapsC X & S₁[x,y,z] holds
z in MapsC X

proof

let x, y, z be object ; :: thesis: ( x in MapsC X & y in MapsC X & S₁[x,y,z] implies z in MapsC X )
assume ( x in MapsC X & y in MapsC X ) ; :: thesis: ( not S₁[x,y,z] or z in MapsC X )
then reconsider l2 = x, l1 = y as Element of MapsC X ;
assume S₁[x,y,z] ; :: thesis: z in MapsC X
then z = l2 * l1 ;
hence z in MapsC X ; :: thesis: verum

end;

consider h being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) such that
A9: for x, y being object holds
( [x,y] in dom h iff ( x in MapsC X & y in MapsC X & ex z being object st S₁[x,y,z] ) ) and
A10: for x, y being object st [x,y] in dom h holds
S₁[x,y,h . (x,y)] from BINOP_1:sch 5(A8, A5);
take h ; :: thesis: ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h . [l2,l1] = l2 * l1 ) )
thus A11: for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom h iff dom l2 = cod l1 ) :: thesis: for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
h . [l2,l1] = l2 * l1

proof

let l2, l1 be Element of MapsC X; :: thesis: ( [l2,l1] in dom h iff dom l2 = cod l1 )
thus ( [l2,l1] in dom h implies dom l2 = cod l1 ) :: thesis: ( dom l2 = cod l1 implies [l2,l1] in dom h )

proof

assume [l2,l1] in dom h ; :: thesis: dom l2 = cod l1
then ex z being object st S₁[l2,l1,z] by A9;
hence dom l2 = cod l1 ; :: thesis: verum

end;

assume dom l2 = cod l1 ; :: thesis: [l2,l1] in dom h
then S₁[l2,l1,l2 * l1] ;
hence [l2,l1] in dom h by A9; :: thesis: verum

end;

let l2, l1 be Element of MapsC X; :: thesis: ( dom l2 = cod l1 implies h . [l2,l1] = l2 * l1 )
assume dom l2 = cod l1 ; :: thesis: h . [l2,l1] = l2 * l1
then [l2,l1] in dom h by A11;
then S₁[l2,l1,h . (l2,l1)] by A10;
hence h . [l2,l1] = l2 * l1 ; :: thesis: verum