let Q be multLoop; :: thesis: for u being Element of Q holds (curry the multF of Q) . u is Permutation of Q
let u be Element of Q; :: thesis: (curry the multF of Q) . u is Permutation of Q
set f = (curry the multF of Q) . u;
deffunc H1( Element of Q) -> Element of Q = u \ $1;
consider g being Function of Q,Q such that
A1: for x being Element of Q holds g . x = H1(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 . (u * x) by FUNCT_5:69
.= H1(u * x) 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
.= u * (g . x) by FUNCT_5:69
.= u * H1(x) 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 Q by FUNCT_2:57, A2, FUNCT_2:31; :: thesis: verum