defpred S₁[ set , set ] means ex g being Function st
( $1 = g & $2 = rng g );
A0: for x, y, z being set st S₁[x,y] & S₁[x,z] holds
y = z ;
consider X being set such that
A1: for x being set holds
( x in X iff ex y being set st
( y in dom v & S₁[y,x] ) ) from TARSKI:sch 1(A0);
set Y = union X;
defpred S₂[ set ] means ex g being Function st
( g = $1 & g * f in dom v );
consider D being set such that
A2: for x being set holds
( x in D iff ( x in Funcs N,(union X) & S₂[x] ) ) from XBOOLE_0:sch 1();
defpred S₃[ set , set ] means ex g being Function st
( g = $1 & $2 = v . (g * f) );
B2: for x being set st x in D holds
ex y being set st S₃[x,y]

proof

let x be set ; :: thesis: ( x in D implies ex y being set st S₃[x,y] )
assume x in D ; :: thesis: ex y being set st S₃[x,y]
then consider y being Function such that
B4: ( y = x & y * f in dom v ) by A2;
take v . (y * f) ; :: thesis: S₃[x,v . (y * f)]
thus S₃[x,v . (y * f)] by B4; :: thesis: verum

end;

consider F being Function such that
A3: ( dom F = D & ( for g being set st g in D holds
S₃[g,F . g] ) ) from CLASSES1:sch 1(B2);
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)

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 ) ) ) ) )

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 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 ) )

hereby :: thesis: ( ex h being Function st
( 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
C2: ( y in a & a in X ) by TARSKI:def 4;
consider z being set such that
C3: ( z in dom v & S₁[z,a] ) by C2, A1;
thus ex h being Function st
( h in dom v & y in rng h ) by C2, C3; :: thesis: verum

end;

given h being Function such that C1: ( h in dom v & y in rng h ) ; :: thesis: y in Y
rng h in X by C1, A1;
hence y in Y by C1, TARSKI:def 4; :: thesis: verum

end;

let a be set ; :: thesis: ( a in dom F iff ( a in Funcs N,Y & ex g being Function st
( 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 A3, A2; :: thesis: verum

end;

let g be Function; :: thesis: ( g in dom F implies F . g = v . (g * f) )
assume g in dom F ; :: thesis: F . g = v . (g * f)
then S₃[g,F . g] by A3;
hence F . g = v . (g * f) ; :: thesis: verum