defpred S1[ object , object ] means ex g being Function st
( g = $1 & $2 = v . (g * f) );
defpred S2[ object ] means ex g being Function st
( g = $1 & g * f in dom v );
defpred S3[ object , object ] means ex g being Function st
( $1 = g & $2 = rng g );
A11: for x, y, z being object st S3[x,y] & S3[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 & S3[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)) & S2[x] ) ) from XBOOLE_0:sch 1();
 A14: for x being object st x in D holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in D implies ex y being object st S1[x,y] )
assume x in D ; :: thesis: ex y being object st S1[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: S1[x,v . (y * f)]
thus S1[x,v . (y * f)] by A15; :: thesis: verum
end;
consider F being Function such that
A16: ( dom F = D & ( for g being object st g in D holds
S1[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) ) )
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
A17: y in a and
A18: a in X by TARSKI:def 4;
ex z being object st
( z in dom v & S3[z,a] ) by A12, A18;
hence ex h being Function st
( h in dom v & y in rng h ) by A17; :: thesis: verum
end;
given h being Function such that A19: h in dom v and
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;
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 A13, A16; :: 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 S1[g,F . g] by A16;
hence F . g = v . (g * f) ; :: thesis: verum