set f = canHom_Rat F;
set c = canHom_Int F;
hereby :: according to VECTSP_1:def 19 :: thesis: canHom_Rat F is multiplicative
let x, y be Element of F_Rat; :: thesis: (canHom_Rat F) . (b1 + b2) = ((canHom_Rat F) . b1) + ((canHom_Rat F) . b2)
reconsider x1 = x, y1 = y as Rational ;
set m = denominator x1;
set n = denominator y1;
set i = numerator x1;
set j = numerator y1;
A1: (canHom_Int F) . (numerator x) = (numerator x) '*' (1. F) by Def8;
A2: (canHom_Int F) . (numerator y) = (numerator y) '*' (1. F) by Def8;
A3: (canHom_Int F) . (numerator (x + y)) = (numerator (x + y)) '*' (1. F) by Def8;
A4: Char F = 0 by Def6;
A5: (((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)) <> 0 by INT_2:5;
A6: (((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)) divides ((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1)) by INT_2:def 2;
A7: (((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)) divides (denominator x1) * (denominator y1) by INT_2:def 2;
A8: ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F) <> 0. F by A4, A5, Def5;
then A9: (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) " <> 0. F by VECTSP_2:13;
A10: ((denominator x1) * (denominator y1)) '*' (1. F) <> 0. F by A4, Def5;
A11: (denominator x1) '*' (1. F) <> 0. F by A4, Def5;
A12: (denominator y1) '*' (1. F) <> 0. F by A4, Def5;
A13: ((canHom_Rat F) . x) + ((canHom_Rat F) . y) = ((canHom_Rat F) . x) + (((canHom_Int F) . (numerator y)) / ((canHom_Int F) . (denominator y))) by Def11
.= (((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x))) + (((canHom_Int F) . (numerator y)) / ((canHom_Int F) . (denominator y))) by Def11
.= (((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) + (((canHom_Int F) . (numerator y)) / ((canHom_Int F) . (denominator y))) by A1, Def8
.= (((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) + (((numerator y1) '*' (1. F)) / ((denominator y1) '*' (1. F))) by A2, Def8
.= ((((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) * (1. F)) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) "))
.= ((((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) * (1 '*' (1. F))) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) by Th59
.= ((((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) * (((denominator y1) div (denominator y1)) '*' (1. F))) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) by INT_1:49
.= ((((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) * (((denominator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) "))) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) by Th96
.= (((numerator x1) '*' (1. F)) * ((((denominator x1) '*' (1. F)) ") * (((denominator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")))) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) by GROUP_1:def 3
.= (((numerator x1) '*' (1. F)) * (((denominator y1) '*' (1. F)) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) ")))) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) by GROUP_1:def 3
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) by GROUP_1:def 3
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + ((((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) * (1. F))
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + ((((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) * (1 '*' (1. F))) by Th59
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + ((((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) * (((denominator x1) div (denominator x1)) '*' (1. F))) by INT_1:49
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + ((((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) ")) * (((denominator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) "))) by Th96
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + (((numerator y1) '*' (1. F)) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")))) by GROUP_1:def 3
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + (((numerator y1) '*' (1. F)) * (((denominator x1) '*' (1. F)) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) ")))) by GROUP_1:def 3
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) + ((((numerator y1) '*' (1. F)) * ((denominator x1) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) "))) by GROUP_1:def 3
.= ((((numerator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) + (((numerator y1) '*' (1. F)) * ((denominator x1) '*' (1. F)))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) ")) by VECTSP_1:def 7
.= ((((numerator x1) * (denominator y1)) '*' (1. F)) + (((numerator y1) '*' (1. F)) * ((denominator x1) '*' (1. F)))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) ")) by Th66
.= ((((numerator x1) * (denominator y1)) '*' (1. F)) + (((numerator y1) * (denominator x1)) '*' (1. F))) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) ")) by Th66
.= ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((denominator y1) '*' (1. F)) ") * (((denominator x1) '*' (1. F)) ")) by Th61
.= ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((denominator y1) '*' (1. F)) * ((denominator x1) '*' (1. F))) ") by A11, A12, VECTSP_2:11
.= ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((denominator y1) * (denominator x1)) '*' (1. F)) ") by Th66
.= ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((1. F) * ((((denominator y1) * (denominator x1)) '*' (1. F)) "))
.= ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ") * (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F))) * ((((denominator x1) * (denominator y1)) '*' (1. F)) ")) by A8, VECTSP_2:def 2
.= ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * (((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ") * (((((denominator x1) * (denominator y1)) '*' (1. F)) ") * (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)))) by GROUP_1:def 3
.= (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) ") * (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F))) by GROUP_1:def 3
.= (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) ") * (((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ") ")) by A8, VECTSP_1:24
.= (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) ") by A9, A10, VECTSP_2:11 ;
A14: (canHom_Rat F) . (x + y) = ((canHom_Int F) . (numerator (x + y))) / ((canHom_Int F) . (denominator (x + y))) by Def11
.= ((numerator (x + y)) '*' (1. F)) * (((denominator (x + y)) '*' (1. F)) ") by A3, Def8
.= (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) div ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) * (((denominator (x + y)) '*' (1. F)) ") by Th35
.= (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) div ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) * (((((denominator x1) * (denominator y1)) div ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) ") by Th35 ;
per cases ( ((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1)) <> 0 or ((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1)) = 0 ) ;
suppose ((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1)) <> 0 ; :: thesis: (canHom_Rat F) . (b1 + b2) = ((canHom_Rat F) . b1) + ((canHom_Rat F) . b2)
hence (canHom_Rat F) . (x + y) = (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) '*' (1. F)) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) div ((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) ") by A14, A5, A6, Th96
.= ((canHom_Rat F) . x) + ((canHom_Rat F) . y) by A13, A5, A7, Th96 ;
:: thesis: verum
end;
suppose A15: ((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1)) = 0 ; :: thesis: (canHom_Rat F) . (b1 + b2) = ((canHom_Rat F) . b1) + ((canHom_Rat F) . b2)
((denominator x1) * (denominator y1)) * 0 = 0 ;
then A16: ( (denominator x1) * (denominator y1) divides 0 & (denominator x1) * (denominator y1) divides (denominator x1) * (denominator y1) ) ;
for a being Integer st a divides 0 & a divides (denominator x1) * (denominator y1) holds
a divides (denominator x1) * (denominator y1) ;
then (((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1)) = (denominator x1) * (denominator y1) by A16, A15, INT_2:def 2;
hence (canHom_Rat F) . (x + y) = (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) div ((denominator x1) * (denominator y1))) '*' (1. F)) * ((1 '*' (1. F)) ") by A14, INT_1:49
.= (((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) div ((denominator x1) * (denominator y1))) '*' (1. F)) * ((1. F) ") by Th59
.= [\(0 / ((denominator x1) * (denominator y1)))/] '*' (1. F) by A15
.= 0 '*' (1. F) by INT_1:25
.= ((0. F) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) * ((((((numerator x1) * (denominator y1)) + ((numerator y1) * (denominator x1))) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) ") by Th58
.= ((canHom_Rat F) . x) + ((canHom_Rat F) . y) by A13, A15, Th58 ;
:: thesis: verum
end;
end;
end;
hereby :: according to GROUP_6:def 6 :: thesis: verum
let x, y be Element of F_Rat; :: thesis: (canHom_Rat F) . (b1 * b2) = ((canHom_Rat F) . b1) * ((canHom_Rat F) . b2)
reconsider x1 = x, y1 = y as Rational ;
set m = denominator x1;
set n = denominator y1;
set i = numerator x1;
set j = numerator y1;
A17: (canHom_Int F) . (numerator x) = (numerator x) '*' (1. F) by Def8;
A18: (canHom_Int F) . (numerator y) = (numerator y) '*' (1. F) by Def8;
A19: (canHom_Int F) . (numerator (x * y)) = (numerator (x * y)) '*' (1. F) by Def8;
A20: Char F = 0 by Def6;
A21: ((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)) <> 0 by INT_2:5;
A22: ((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)) divides (numerator x1) * (numerator y1) by INT_2:def 2;
A23: ((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)) divides (denominator x1) * (denominator y1) by INT_2:def 2;
A24: (((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F) <> 0. F by A20, A21, Def5;
then A25: ((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) " <> 0. F by VECTSP_2:13;
A26: ((denominator x1) * (denominator y1)) '*' (1. F) <> 0. F by A20, Def5;
A27: (denominator x1) '*' (1. F) <> 0. F by A20, Def5;
A28: (denominator y1) '*' (1. F) <> 0. F by A20, Def5;
A29: ((canHom_Rat F) . x) * ((canHom_Rat F) . y) = ((canHom_Rat F) . x) * (((canHom_Int F) . (numerator y)) / ((canHom_Int F) . (denominator y))) by Def11
.= (((canHom_Int F) . (numerator x)) / ((canHom_Int F) . (denominator x))) * (((canHom_Int F) . (numerator y)) / ((canHom_Int F) . (denominator y))) by Def11
.= (((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) * (((canHom_Int F) . (numerator y)) / ((canHom_Int F) . (denominator y))) by A17, Def8
.= (((numerator x1) '*' (1. F)) * (((denominator x1) '*' (1. F)) ")) * (((numerator y1) '*' (1. F)) / ((denominator y1) '*' (1. F))) by A18, Def8
.= ((numerator x1) '*' (1. F)) * ((((denominator x1) '*' (1. F)) ") * (((numerator y1) '*' (1. F)) * (((denominator y1) '*' (1. F)) "))) by GROUP_1:def 3
.= ((numerator x1) '*' (1. F)) * (((((denominator x1) '*' (1. F)) ") * (((denominator y1) '*' (1. F)) ")) * ((numerator y1) '*' (1. F))) by GROUP_1:def 3
.= (((numerator x1) '*' (1. F)) * ((numerator y1) '*' (1. F))) * ((((denominator x1) '*' (1. F)) ") * (((denominator y1) '*' (1. F)) ")) by GROUP_1:def 3
.= (((numerator x1) * (numerator y1)) '*' (1. F)) * ((((denominator x1) '*' (1. F)) ") * (((denominator y1) '*' (1. F)) ")) by Th66
.= (((numerator x1) * (numerator y1)) '*' (1. F)) * ((((denominator x1) '*' (1. F)) * ((denominator y1) '*' (1. F))) ") by A27, A28, VECTSP_2:11
.= (((numerator x1) * (numerator y1)) '*' (1. F)) * ((((denominator x1) * (denominator y1)) '*' (1. F)) ") by Th66
.= (((numerator x1) * (numerator y1)) '*' (1. F)) * ((1. F) * ((((denominator x1) * (denominator y1)) '*' (1. F)) "))
.= (((numerator x1) * (numerator y1)) '*' (1. F)) * (((((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ") * ((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F))) * ((((denominator x1) * (denominator y1)) '*' (1. F)) ")) by A24, VECTSP_2:def 2
.= (((numerator x1) * (numerator y1)) '*' (1. F)) * ((((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ") * (((((denominator x1) * (denominator y1)) '*' (1. F)) ") * ((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)))) by GROUP_1:def 3
.= ((((numerator x1) * (numerator y1)) '*' (1. F)) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) ") * ((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F))) by GROUP_1:def 3
.= ((((numerator x1) * (numerator y1)) '*' (1. F)) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) ") * ((((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ") ")) by A24, VECTSP_1:24
.= ((((numerator x1) * (numerator y1)) '*' (1. F)) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) ") by A25, A26, VECTSP_2:11 ;
A30: (canHom_Rat F) . (x * y) = ((canHom_Int F) . (numerator (x * y))) / ((canHom_Int F) . (denominator (x * y))) by Def11
.= ((numerator (x * y)) '*' (1. F)) * (((denominator (x * y)) '*' (1. F)) ") by A19, Def8
.= ((((numerator x1) * (numerator y1)) div (((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) * (((denominator (x * y)) '*' (1. F)) ") by Th39
.= ((((numerator x1) * (numerator y1)) div (((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) * (((((denominator x1) * (denominator y1)) div (((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) ") by Th39 ;
per cases ( (numerator x1) * (numerator y1) <> 0 or (numerator x1) * (numerator y1) = 0 ) ;
suppose (numerator x1) * (numerator y1) <> 0 ; :: thesis: (canHom_Rat F) . (b1 * b2) = ((canHom_Rat F) . b1) * ((canHom_Rat F) . b2)
hence (canHom_Rat F) . (x * y) = ((((numerator x1) * (numerator y1)) '*' (1. F)) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) div (((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)))) '*' (1. F)) ") by A30, A21, A22, Th96
.= ((canHom_Rat F) . x) * ((canHom_Rat F) . y) by A29, A21, A23, Th96 ;
:: thesis: verum
end;
suppose A31: (numerator x1) * (numerator y1) = 0 ; :: thesis: (canHom_Rat F) . (b1 * b2) = ((canHom_Rat F) . b1) * ((canHom_Rat F) . b2)
((denominator x1) * (denominator y1)) * 0 = 0 ;
then A32: ( (denominator x1) * (denominator y1) divides 0 & (denominator x1) * (denominator y1) divides (denominator x1) * (denominator y1) ) ;
for a being Integer st a divides 0 & a divides (denominator x1) * (denominator y1) holds
a divides (denominator x1) * (denominator y1) ;
then ((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1)) = (denominator x1) * (denominator y1) by A32, A31, INT_2:def 2;
hence (canHom_Rat F) . (x * y) = ((((numerator x1) * (numerator y1)) div ((denominator x1) * (denominator y1))) '*' (1. F)) * ((1 '*' (1. F)) ") by A30, INT_1:49
.= ((((numerator x1) * (numerator y1)) div ((denominator x1) * (denominator y1))) '*' (1. F)) * ((1. F) ") by Th59
.= [\(0 / ((denominator x1) * (denominator y1)))/] '*' (1. F) by A31
.= 0 '*' (1. F) by INT_1:25
.= ((0. F) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) * (((((denominator x1) * (denominator y1)) '*' (1. F)) * (((((numerator x1) * (numerator y1)) gcd ((denominator x1) * (denominator y1))) '*' (1. F)) ")) ") by Th58
.= ((canHom_Rat F) . x) * ((canHom_Rat F) . y) by A29, A31, Th58 ;
:: thesis: verum
end;
end;
end;