defpred S1[ object , object , object ] 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 object st x in MapsT X & y in MapsT X & S1[x,y,z1] & S1[x,y,z2] holds
z1 = z2
proof
let x,
y,
z1,
z2 be
object ;
( x in MapsT X & y in MapsT X & S1[x,y,z1] & S1[x,y,z2] implies z1 = z2 )
assume
(
x in MapsT X &
y in MapsT X )
;
( not S1[x,y,z1] or not S1[x,y,z2] or z1 = z2 )
then reconsider m2 =
x,
m1 =
y as
Element of
MapsT X ;
assume that A6:
S1[
x,
y,
z1]
and A7:
S1[
x,
y,
z2]
;
z1 = z2
z1 = m2 * m1
by A6;
hence
z1 = z2
by A7;
verum
end;
A8:
for x, y, z being object st x in MapsT X & y in MapsT X & S1[x,y,z] holds
z in MapsT X
consider h being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) such that
A9:
for x, y being object holds
( [x,y] in dom h iff ( x in MapsT X & y in MapsT X & 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 BINOP_1:sch 5(A8, A5);
take
h
; ( ( 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 )
for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
h . [m2,m1] = m2 * m1
let m2, m1 be Element of MapsT X; ( dom m2 = cod m1 implies h . [m2,m1] = m2 * m1 )
assume
dom m2 = cod m1
; 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
; verum