thus P => Q is one-to-one :: according to FUNCT_2:def 4 :: thesis: P => Q is onto
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (P => Q) or not x2 in dom (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:17
.= (Q * f1) * ((P ") * P) by FUNCT_2:61
.= ((Q * f2) * (P ")) * P by A1, RELAT_1:36
.= (Q * f2) * ((P ") * P) by RELAT_1:36
.= (Q * f2) * (id A) by FUNCT_2:61
.= Q * f2 by FUNCT_2:17 ;
f1 = (id B) * f1 by FUNCT_2:17
.= ((Q ") * Q) * f1 by FUNCT_2:61
.= (Q ") * (Q * f2) by A2, RELAT_1:36
.= ((Q ") * Q) * f2 by RELAT_1:36
.= (id B) * f2 by FUNCT_2:61
.= f2 by FUNCT_2:17 ;
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= K435((Funcs (A,B)),(P => Q))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (A,B) or x in K435((Funcs (A,B)),(P => Q)) )
assume x in Funcs (A,B) ; :: thesis: x in K435((Funcs (A,B)),(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:8;
(P => Q) . (((Q ") * f) * P) = (Q * (((Q ") * f) * P)) * (P ") by Def1
.= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36
.= (((Q * (Q ")) * f) * P) * (P ") by RELAT_1:36
.= (((id B) * f) * P) * (P ") by FUNCT_2:61
.= (f * P) * (P ") by FUNCT_2:17
.= f * (P * (P ")) by RELAT_1:36
.= f * (id A) by FUNCT_2:61
.= f by FUNCT_2:17 ;
hence x in rng (P => Q) by A3, FUNCT_1:def 3; :: thesis: verum