[:P,Q:] is bijective

proof

thus [:P,Q:] is one-to-one ; :: according to FUNCT_2:def 4 :: thesis: [:P,Q:] is onto
( rng P = A & rng Q = B ) by FUNCT_2:def 3;
hence rng [:P,Q:] = [:A,B:] by FUNCT_3:67; :: according to FUNCT_2:def 3 :: thesis: verum

end;

hence for b₁ being Function of [:A,B:],[:A,B:] st b₁ = [:P,Q:] holds
b₁ is bijective ; :: thesis: verum