A5: for x being Element of F1() ex y being Element of F1() st P1[x,y] by A1;
consider f being Function of F1(),F1() such that
A6: for x being Element of F1() holds P1[x,f . x] from FUNCT_2:sch 3(A5);
now :: thesis: for y being object st y in F1() holds
y in rng f
let y be object ; :: thesis: ( y in F1() implies y in rng f )
assume A7: y in F1() ; :: thesis: y in rng f
then consider x being Element of F1() such that
A8: P1[x,y] by A2;
P1[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 F1() c= rng f by TARSKI:def 3;
then A9: rng f = F1() by XBOOLE_0:def 10;
now :: thesis: for x1, x2 being object st x1 in F1() & x2 in F1() & f . x1 = f . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in F1() & x2 in F1() & f . x1 = f . x2 implies x1 = x2 )
assume that
A10: x1 in F1() and
A11: x2 in F1() ; :: thesis: ( f . x1 = f . x2 implies x1 = x2 )
A12: f . x1 is Element of F1() by A10, FUNCT_2:5;
( P1[x1,f . x1] & P1[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 F1() by A9, FUNCT_2:57;
take f ; :: thesis: for x, y being Element of F1() holds
( f . x = y iff P1[x,y] )
let x, y be Element of F1(); :: thesis: ( f . x = y iff P1[x,y] )
thus ( f . x = y implies P1[x,y] ) by A6; :: thesis: ( P1[x,y] implies f . x = y )
assume A13: P1[x,y] ; :: thesis: f . x = y
P1[x,f . x] by A6;
hence f . x = y by A4, A13; :: thesis: verum