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

proof

let x, y, z1, z2 be set ; :: thesis: ( x in Maps V & y in Maps V & S₁[x,y,z1] & S₁[x,y,z2] implies z1 = z2 )
assume ( x in Maps V & y in Maps V ) ; :: thesis: ( not S₁[x,y,z1] or not S₁[x,y,z2] or z1 = z2 )
then reconsider m2 = x, m1 = y as Element of Maps V ;
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 Maps V & y in Maps V & S₁[x,y,z] holds
z in Maps V

proof

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

end;

consider h being PartFunc of [:(Maps V),(Maps V):],(Maps V) such that
A9: for x, y being set holds
( [x,y] in dom h iff ( x in Maps V & y in Maps V & 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 Maps V holds
( [m2,m1] in dom h iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1 ) )
thus A11: for m2, m1 being Element of Maps V holds
( [m2,m1] in dom h iff dom m2 = cod m1 ) :: thesis: for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1

proof

let m2, m1 be Element of Maps V; :: 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 Maps V; :: 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