defpred S_{1}[ object , object ] means ex g being Function st

( g = $1 & $2 = v . (g * f) );

defpred S_{2}[ object ] means ex g being Function st

( g = $1 & g * f in dom v );

defpred S_{3}[ object , object ] means ex g being Function st

( $1 = g & $2 = rng g );

A11: for x, y, z being object st S_{3}[x,y] & S_{3}[x,z] holds

y = z ;

consider X being set such that

A12: for x being object holds

( x in X iff ex y being object st

( y in dom v & S_{3}[y,x] ) )
from TARSKI:sch 1(A11);

set Y = union X;

consider D being set such that

A13: for x being object holds

( x in D iff ( x in Funcs (N,(union X)) & S_{2}[x] ) )
from XBOOLE_0:sch 1();

A14: for x being object st x in D holds

ex y being object st S_{1}[x,y]

A16: ( dom F = D & ( for g being object st g in D holds

S_{1}[g,F . g] ) )
from CLASSES1:sch 1(A14);

take F ; :: thesis: ( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom F holds

F . g = v . (g * f) ) )

assume g in dom F ; :: thesis: F . g = v . (g * f)

then S_{1}[g,F . g]
by A16;

hence F . g = v . (g * f) ; :: thesis: verum

( g = $1 & $2 = v . (g * f) );

defpred S

( g = $1 & g * f in dom v );

defpred S

( $1 = g & $2 = rng g );

A11: for x, y, z being object st S

y = z ;

consider X being set such that

A12: for x being object holds

( x in X iff ex y being object st

( y in dom v & S

set Y = union X;

consider D being set such that

A13: for x being object holds

( x in D iff ( x in Funcs (N,(union X)) & S

A14: for x being object st x in D holds

ex y being object st S

proof

consider F being Function such that
let x be object ; :: thesis: ( x in D implies ex y being object st S_{1}[x,y] )

assume x in D ; :: thesis: ex y being object st S_{1}[x,y]

then consider y being Function such that

A15: y = x and

y * f in dom v by A13;

take v . (y * f) ; :: thesis: S_{1}[x,v . (y * f)]

thus S_{1}[x,v . (y * f)]
by A15; :: thesis: verum

end;assume x in D ; :: thesis: ex y being object st S

then consider y being Function such that

A15: y = x and

y * f in dom v by A13;

take v . (y * f) ; :: thesis: S

thus S

A16: ( dom F = D & ( for g being object st g in D holds

S

take F ; :: thesis: ( ex Y being set st

( ( for y being set holds

( y in Y iff ex h being Function st

( h in dom v & y in rng h ) ) ) & ( for a being set holds

( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom F holds

F . g = v . (g * f) ) )

hereby :: thesis: for g being Function st g in dom F holds

F . g = v . (g * f)

let g be Function; :: thesis: ( g in dom F implies F . g = v . (g * f) )F . g = v . (g * f)

take Y = union X; :: thesis: ( ( for y being set holds

( ( y in Y implies ex h being Function st

( h in dom v & y in rng h ) ) & ( ex h being Function st

( h in dom v & y in rng h ) implies y in Y ) ) ) & ( for a being set holds

( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) )

( a = g & g * f in dom v ) ) )

thus ( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) by A13, A16; :: thesis: verum

end;( ( y in Y implies ex h being Function st

( h in dom v & y in rng h ) ) & ( ex h being Function st

( h in dom v & y in rng h ) implies y in Y ) ) ) & ( for a being set holds

( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) ) )

hereby :: thesis: for a being set holds

( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) )

let a be set ; :: thesis: ( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st ( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) )

let y be set ; :: thesis: ( ( y in Y implies ex h being Function st

( h in dom v & y in rng h ) ) & ( ex h being Function st

( h in dom v & y in rng h ) implies y in Y ) )

A20: y in rng h ; :: thesis: y in Y

rng h in X by A12, A19;

hence y in Y by A20, TARSKI:def 4; :: thesis: verum

end;( h in dom v & y in rng h ) ) & ( ex h being Function st

( h in dom v & y in rng h ) implies y in Y ) )

hereby :: thesis: ( ex h being Function st

( h in dom v & y in rng h ) implies y in Y )

given h being Function such that A19:
h in dom v
and ( h in dom v & y in rng h ) implies y in Y )

assume
y in Y
; :: thesis: ex h being Function st

( h in dom v & y in rng h )

then consider a being set such that

A17: y in a and

A18: a in X by TARSKI:def 4;

ex z being object st

( z in dom v & S_{3}[z,a] )
by A12, A18;

hence ex h being Function st

( h in dom v & y in rng h ) by A17; :: thesis: verum

end;( h in dom v & y in rng h )

then consider a being set such that

A17: y in a and

A18: a in X by TARSKI:def 4;

ex z being object st

( z in dom v & S

hence ex h being Function st

( h in dom v & y in rng h ) by A17; :: thesis: verum

A20: y in rng h ; :: thesis: y in Y

rng h in X by A12, A19;

hence y in Y by A20, TARSKI:def 4; :: thesis: verum

( a = g & g * f in dom v ) ) )

thus ( a in dom F iff ( a in Funcs (N,Y) & ex g being Function st

( a = g & g * f in dom v ) ) ) by A13, A16; :: thesis: verum

assume g in dom F ; :: thesis: F . g = v . (g * f)

then S

hence F . g = v . (g * f) ; :: thesis: verum