let F be Field; :: thesis: for a being Element of F
for b being non zero Element of F holds (a / b) ^2 = (a ^2) / (b ^2)
let a be Element of F; :: thesis: for b being non zero Element of F holds (a / b) ^2 = (a ^2) / (b ^2)
let b be non zero Element of F; :: thesis: (a / b) ^2 = (a ^2) / (b ^2)
H1: b <> 0. F ;
thus (a / b) ^2 = a * ((b ") * (a * (b "))) by GROUP_1:def 3
.= a * (a * ((b ") * (b "))) by GROUP_1:def 3
.= (a * a) * ((b ") * (b ")) by GROUP_1:def 3
.= (a ^2) / (b ^2) by VECTSP_2:11, H1 ; :: thesis: verum