thus P => Q is one-to-one :: according to FUNCT_2:def 4 :: thesis: P => Q is onto

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (P => Q) or not x2 in proj1 (P => Q) or not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 )
assume ( x1 in dom (P => Q) & x2 in dom (P => Q) ) ; :: thesis: ( not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 )
then reconsider f1 = x1, f2 = x2 as Element of Funcs A,B by FUNCT_2:def 1;
assume (P => Q) . x1 = (P => Q) . x2 ; :: thesis: x1 = x2
then A1: (Q * f1) * (P " ) = (P => Q) . f2 by Def1
.= (Q * f2) * (P " ) by Def1 ;
A2: Q * f1 = (Q * f1) * (id A) by FUNCT_2:23
.= (Q * f1) * ((P " ) * P) by FUNCT_2:88
.= ((Q * f2) * (P " )) * P by A1, RELAT_1:55
.= (Q * f2) * ((P " ) * P) by RELAT_1:55
.= (Q * f2) * (id A) by FUNCT_2:88
.= Q * f2 by FUNCT_2:23 ;
f1 = (id B) * f1 by FUNCT_2:23
.= ((Q " ) * Q) * f1 by FUNCT_2:88
.= (Q " ) * (Q * f2) by A2, RELAT_1:55
.= ((Q " ) * Q) * f2 by RELAT_1:55
.= (id B) * f2 by FUNCT_2:88
.= f2 by FUNCT_2:23 ;
hence x1 = x2 ; :: thesis: verum

end;

thus rng (P => Q) c= Funcs A,B by RELAT_1:def 19; :: according to FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: Funcs A,B c= proj2 (P => Q)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs A,B or x in proj2 (P => Q) )
assume x in Funcs A,B ; :: thesis: x in proj2 (P => Q)
then x is Element of Funcs A,B ;
then reconsider f = x as Function of A,B ;
dom (P => Q) = Funcs A,B by FUNCT_2:def 1;
then A3: ((Q " ) * f) * P in dom (P => Q) by FUNCT_2:11;
(P => Q) . (((Q " ) * f) * P) = (Q * (((Q " ) * f) * P)) * (P " ) by Def1
.= ((Q * ((Q " ) * f)) * P) * (P " ) by RELAT_1:55
.= (((Q * (Q " )) * f) * P) * (P " ) by RELAT_1:55
.= (((id B) * f) * P) * (P " ) by FUNCT_2:88
.= (f * P) * (P " ) by FUNCT_2:23
.= f * (P * (P " )) by RELAT_1:55
.= f * (id A) by FUNCT_2:88
.= f by FUNCT_2:23 ;
hence x in rng (P => Q) by A3, FUNCT_1:def 5; :: thesis: verum