let F be Function; :: thesis: for x, y being object st x in dom F & y in dom F holds
F, Swap (F,x,y) are_fiberwise_equipotent
let x, y be object ; :: thesis: ( x in dom F & y in dom F implies F, Swap (F,x,y) are_fiberwise_equipotent )
assume A1: ( x in dom F & y in dom F ) ; :: thesis: F, Swap (F,x,y) are_fiberwise_equipotent
A2: dom (Swap (F,x,y)) = dom F by FUNCT_7:99;
A3: dom (Swap ((id (dom F)),x,y)) = dom (id (dom F)) by FUNCT_7:99;
A4: rng (Swap ((id (dom F)),x,y)) = rng (id (dom F)) by FUNCT_7:103;
Swap (F,x,y) = F * (Swap ((id (dom F)),x,y)) by A1, Th27;
hence F, Swap (F,x,y) are_fiberwise_equipotent by A1, A2, A3, A4, CLASSES1:77; :: thesis: verum