let A, B be set ; :: thesis: for P being Permutation of A
for Q being Permutation of B holds [:P,Q:] is bijective
let P be Permutation of A; :: thesis: for Q being Permutation of B holds [:P,Q:] is bijective
let Q be Permutation of B; :: thesis: [:P,Q:] is bijective
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