A5: for x being Element of F₁() ex y being Element of F₁() st P₁[x,y] by A1;
consider f being Function of F₁(),F₁() such that
A6: for x being Element of F₁() holds P₁[x,f . x] from FUNCT_2:sch 3(A5);

now :: thesis: for y being object st y in F₁() holds
y in rng f

let y be object ; :: thesis: ( y in F₁() implies y in rng f )
assume A7: y in F₁() ; :: thesis: y in rng f
then consider x being Element of F₁() such that
A8: P₁[x,y] by A2;
P₁[x,f . x] by A6;
then f . x = y by A4, A7, A8;
hence y in rng f by FUNCT_2:4; :: thesis: verum

end;

then F₁() c= rng f by TARSKI:def 3;
then A9: rng f = F₁() by XBOOLE_0:def 10;

now :: thesis: for x1, x2 being object st x1 in F₁() & x2 in F₁() & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in F₁() & x2 in F₁() & f . x1 = f . x2 implies x1 = x2 )
assume that
A10: x1 in F₁() and
A11: x2 in F₁() ; :: thesis: ( f . x1 = f . x2 implies x1 = x2 )
A12: f . x1 is Element of F₁() by A10, FUNCT_2:5;
( P₁[x1,f . x1] & P₁[x2,f . x2] ) by A6, A10, A11;
hence ( f . x1 = f . x2 implies x1 = x2 ) by A3, A10, A11, A12; :: thesis: verum

end;

then f is one-to-one by FUNCT_2:19;
then reconsider f = f as Permutation of F₁() by A9, FUNCT_2:57;
take f ; :: thesis: for x, y being Element of F₁() holds
( f . x = y iff P₁[x,y] )
let x, y be Element of F₁(); :: thesis: ( f . x = y iff P₁[x,y] )
thus ( f . x = y implies P₁[x,y] ) by A6; :: thesis: ( P₁[x,y] implies f . x = y )
assume A13: P₁[x,y] ; :: thesis: f . x = y
P₁[x,f . x] by A6;
hence f . x = y by A4, A13; :: thesis: verum