defpred S1[ object , object , object ] 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 object st x in Maps V & y in Maps V & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
proof
let x, y, z1, z2 be object ; :: thesis: ( x in Maps V & y in Maps V & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume ( x in Maps V & y in Maps V ) ; :: thesis: ( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 )
then reconsider m2 = x, m1 = y as Element of Maps V ;
assume that
A6: S1[x,y,z1] and
A7: S1[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 object st x in Maps V & y in Maps V & S1[x,y,z] holds
z in Maps V
proof
let x, y, z be object ; :: thesis: ( x in Maps V & y in Maps V & S1[x,y,z] implies z in Maps V )
assume ( x in Maps V & y in Maps V ) ; :: thesis: ( not S1[x,y,z] or z in Maps V )
then reconsider m2 = x, m1 = y as Element of Maps V ;
assume S1[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 object holds
( [x,y] in dom h iff ( x in Maps V & y in Maps V & ex z being object st S1[x,y,z] ) ) and
A10: for x, y being object st [x,y] in dom h holds
S1[x,y,h . (x,y)] from 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 object st S1[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 S1[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 S1[m2,m1,h . (m2,m1)] by A10;
hence h . [m2,m1] = m2 * m1 ; :: thesis: verum