let F be 0 -characteristic Field; :: thesis: for i, j being non zero Integer st j divides i holds
(i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ")
let i, j be non zero Integer; :: thesis: ( j divides i implies (i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ") )
A1: Char F = 0 by Def6;
assume j divides i ; :: thesis: (i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ")
then consider k being Integer such that
A2: i = j * k ;
A3: (i div j) * j = [\(k * (j / j))/] * j by A2
.= [\(k * 1)/] * j by XCMPLX_1:60
.= i by A2 ;
A4: j '*' (1. F) <> 0. F

proof

per cases ( j > 0 or j < 0 ) ;

suppose j > 0 ; :: thesis: j '*' (1. F) <> 0. F

then j is Element of NAT by INT_1:3;
hence j '*' (1. F) <> 0. F by A1, Def5; :: thesis: verum

end;

suppose j < 0 ; :: thesis: j '*' (1. F) <> 0. F

then A5: - j is Element of NAT by INT_1:3;
A6: j '*' (1. F) = (- (- j)) '*' (1. F)
.= - ((- j) '*' (1. F)) by Th62 ;

now :: thesis: ( j '*' (1. F) = 0. F implies (- j) '*' (1. F) = 0. F )

assume j '*' (1. F) = 0. F ; :: thesis: (- j) '*' (1. F) = 0. F
then - (- ((- j) '*' (1. F))) = 0. F by A6;
hence (- j) '*' (1. F) = 0. F ; :: thesis: verum

end;

hence j '*' (1. F) <> 0. F by A5, A1, Def5; :: thesis: verum

end;

end;

end;

A7: i '*' (1. F) <> 0. F

proof

per cases ( i > 0 or i < 0 ) ;

suppose i > 0 ; :: thesis: i '*' (1. F) <> 0. F

then i is Element of NAT by INT_1:3;
hence i '*' (1. F) <> 0. F by A1, Def5; :: thesis: verum

end;

suppose i < 0 ; :: thesis: i '*' (1. F) <> 0. F

then A8: - i is Element of NAT by INT_1:3;
A9: i '*' (1. F) = (- (- i)) '*' (1. F)
.= - ((- i) '*' (1. F)) by Th62 ;

now :: thesis: ( i '*' (1. F) = 0. F implies (- i) '*' (1. F) = 0. F )

assume i '*' (1. F) = 0. F ; :: thesis: (- i) '*' (1. F) = 0. F
then - (- ((- i) '*' (1. F))) = 0. F by A9;
hence (- i) '*' (1. F) = 0. F ; :: thesis: verum

end;

hence i '*' (1. F) <> 0. F by A8, A1, Def5; :: thesis: verum

end;

end;

end;

(((i div j) '*' (1. F)) * ((i '*' (1. F)) ")) * (j '*' (1. F)) = ((i '*' (1. F)) ") * (((i div j) '*' (1. F)) * (j '*' (1. F))) by GROUP_1:def 3
.= ((i '*' (1. F)) ") * (((i div j) * j) '*' (1. F)) by Th66
.= 1. F by A3, A7, VECTSP_1:def 10 ;
then (j '*' (1. F)) " = ((i div j) '*' (1. F)) * ((i '*' (1. F)) ") by A4, VECTSP_1:def 10;
hence (i '*' (1. F)) * ((j '*' (1. F)) ") = ((i '*' (1. F)) * ((i '*' (1. F)) ")) * ((i div j) '*' (1. F)) by GROUP_1:def 3
.= (1. F) * ((i div j) '*' (1. F)) by A7, VECTSP_1:def 10
.= (i div j) '*' (1. F) ;
:: thesis: verum