A5:
for x being Element of F_{1}() ex y being Element of F_{1}() st P_{1}[x,y]
by A1;

consider f being Function of F_{1}(),F_{1}() such that

A6: for x being Element of F_{1}() holds P_{1}[x,f . x]
from FUNCT_2:sch 3(A5);

_{1}() c= rng f
by TARSKI:def 3;

then A9: rng f = F_{1}()
by XBOOLE_0:def 10;

then reconsider f = f as Permutation of F_{1}() by A9, FUNCT_2:57;

take f ; :: thesis: for x, y being Element of F_{1}() holds

( f . x = y iff P_{1}[x,y] )

let x, y be Element of F_{1}(); :: thesis: ( f . x = y iff P_{1}[x,y] )

thus ( f . x = y implies P_{1}[x,y] )
by A6; :: thesis: ( P_{1}[x,y] implies f . x = y )

assume A13: P_{1}[x,y]
; :: thesis: f . x = y

P_{1}[x,f . x]
by A6;

hence f . x = y by A4, A13; :: thesis: verum

consider f being Function of F

A6: for x being Element of F

now :: thesis: for y being object st y in F_{1}() holds

y in rng f

then
Fy in rng f

let y be object ; :: thesis: ( y in F_{1}() implies y in rng f )

assume A7: y in F_{1}()
; :: thesis: y in rng f

then consider x being Element of F_{1}() such that

A8: P_{1}[x,y]
by A2;

P_{1}[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;assume A7: y in F

then consider x being Element of F

A8: P

P

then f . x = y by A4, A7, A8;

hence y in rng f by FUNCT_2:4; :: thesis: verum

then A9: rng f = F

now :: thesis: for x1, x2 being object st x1 in F_{1}() & x2 in F_{1}() & f . x1 = f . x2 holds

x1 = x2

then
f is one-to-one
by FUNCT_2:19;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in F_{1}() & x2 in F_{1}() & f . x1 = f . x2 implies x1 = x2 )

assume that

A10: x1 in F_{1}()
and

A11: x2 in F_{1}()
; :: thesis: ( f . x1 = f . x2 implies x1 = x2 )

A12: f . x1 is Element of F_{1}()
by A10, FUNCT_2:5;

( P_{1}[x1,f . x1] & P_{1}[x2,f . x2] )
by A6, A10, A11;

hence ( f . x1 = f . x2 implies x1 = x2 ) by A3, A10, A11, A12; :: thesis: verum

end;assume that

A10: x1 in F

A11: x2 in F

A12: f . x1 is Element of F

( P

hence ( f . x1 = f . x2 implies x1 = x2 ) by A3, A10, A11, A12; :: thesis: verum

then reconsider f = f as Permutation of F

take f ; :: thesis: for x, y being Element of F

( f . x = y iff P

let x, y be Element of F

thus ( f . x = y implies P

assume A13: P

P

hence f . x = y by A4, A13; :: thesis: verum