let f1, f2, f3, f4 be Element of RAT_Music; ( the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) iff the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) )
set MS = RAT_Music ;
reconsider x = [f1,f2], y = [f3,f4] as Element of [:RATPLUS,RATPLUS:] by ZFMISC_1:def 2;
consider y9, z9 being Element of RATPLUS such that
A1:
x = [y9,z9]
and
A2:
RAT_ratio . x = RAT_ratio (y9,z9)
by Def05;
consider y99, z99 being Element of RATPLUS such that
A3:
y = [y99,z99]
and
A4:
RAT_ratio . y = RAT_ratio (y99,z99)
by Def05;
reconsider x1 = [z9,y9], y1 = [z99,y99] as Element of [:RATPLUS,RATPLUS:] ;
consider y19, z19 being Element of RATPLUS such that
A5:
x1 = [y19,z19]
and
A6:
RAT_ratio . x1 = RAT_ratio (y19,z19)
by Def05;
consider y199, z199 being Element of RATPLUS such that
A7:
y1 = [y199,z199]
and
A8:
RAT_ratio . y1 = RAT_ratio (y199,z199)
by Def05;
A9:
( f1 = y9 & f2 = z9 & f3 = y99 & f4 = z99 )
by A1, A3, XTUPLE_0:1;
then A10:
( f1 = z19 & f2 = y19 & f3 = z199 & f4 = y199 )
by A5, A7, XTUPLE_0:1;
A11:
( the Ratio of RAT_Music . (f2,f1) = RAT_ratio (y19,z19) & the Ratio of RAT_Music . (f4,f3) = RAT_ratio (y199,z199) )
by A9, BINOP_1:def 1, A6, A8;
hereby ( the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) implies the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4) )
assume A12:
the
Ratio of
RAT_Music . (
f1,
f2)
= the
Ratio of
RAT_Music . (
f3,
f4)
;
the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3) RAT_ratio (
y9,
z9) =
RAT_ratio . (
f1,
f2)
by A2, BINOP_1:def 1
.=
RAT_ratio (
y99,
z99)
by A12, A4, BINOP_1:def 1
;
hence
the
Ratio of
RAT_Music . (
f2,
f1)
= the
Ratio of
RAT_Music . (
f4,
f3)
by A9, A10, A11, Th13;
verum
end;
assume A13:
the Ratio of RAT_Music . (f2,f1) = the Ratio of RAT_Music . (f4,f3)
; the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4)
RAT_ratio . (f1,f2) =
RAT_ratio (z19,y19)
by BINOP_1:def 1, A9, A10, A2
.=
RAT_ratio (z199,y199)
by A13, A11, Th13
.=
RAT_ratio . (f3,f4)
by BINOP_1:def 1, A9, A10, A4
;
hence
the Ratio of RAT_Music . (f1,f2) = the Ratio of RAT_Music . (f3,f4)
; verum