let Q be multLoop; :: thesis: for u being Element of Q holds (curry' the multF of Q) . u is Permutation of the carrier of Q
let u be Element of Q; :: thesis: (curry' the multF of Q) . u is Permutation of the carrier of Q
set f = (curry' the multF of Q) . u;
deffunc H₁( Element of Q) -> Element of Q = $1 / u;
consider g being Function of Q,Q such that
A1: for x being Element of Q holds g . x = H₁(x) from FUNCT_2:sch 4();
for x being Element of Q holds (g * ((curry' the multF of Q) . u)) . x = (id Q) . x

proof

let x be Element of Q; :: thesis: (g * ((curry' the multF of Q) . u)) . x = (id Q) . x
(g * ((curry' the multF of Q) . u)) . x = g . (((curry' the multF of Q) . u) . x) by FUNCT_2:15
.= g . (x * u) by FUNCT_5:70
.= H₁(x * u) by A1
.= (id Q) . x ;
hence (g * ((curry' the multF of Q) . u)) . x = (id Q) . x ; :: thesis: verum

end;

then A2: g * ((curry' the multF of Q) . u) = id Q by FUNCT_2:def 8;
A3: for x being Element of Q holds (((curry' the multF of Q) . u) * g) . x = (id Q) . x

proof

let x be Element of Q; :: thesis: (((curry' the multF of Q) . u) * g) . x = (id Q) . x
(((curry' the multF of Q) . u) * g) . x = ((curry' the multF of Q) . u) . (g . x) by FUNCT_2:15
.= (g . x) * u by FUNCT_5:70
.= H₁(x) * u by A1
.= (id Q) . x ;
hence (((curry' the multF of Q) . u) * g) . x = (id Q) . x ; :: thesis: verum

end;

rng ((curry' the multF of Q) . u) = the carrier of Q by A3, FUNCT_2:18, FUNCT_2:def 8;
hence (curry' the multF of Q) . u is Permutation of the carrier of Q by FUNCT_2:57, A2, FUNCT_2:31; :: thesis: verum