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

proof

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

end;

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

proof

let x, y, z be set ; :: thesis: ( x in MapsT X & y in MapsT X & S₁[x,y,z] implies z in MapsT X )
assume ( x in MapsT X & y in MapsT X ) ; :: thesis: ( not S₁[x,y,z] or z in MapsT X )
then reconsider m2 = x, m1 = y as Element of MapsT X ;
assume S₁[x,y,z] ; :: thesis: z in MapsT X
then z = m2 * m1 ;
hence z in MapsT X ; :: thesis: verum

end;

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

proof

let m2, m1 be Element of MapsT X; :: thesis: ( [m2,m1] in dom h iff dom m2 = cod m1 )
thus ( [m2,m1] in dom h implies dom m2 = cod m1 ) :: thesis: ( dom m2 = cod m1 implies [m2,m1] in dom h )

proof

assume [m2,m1] in dom h ; :: thesis: dom m2 = cod m1
then ex z being set st S₁[m2,m1,z] by A9;
hence dom m2 = cod m1 ; :: thesis: verum

end;

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

end;

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