let F1, F2 be Function; :: 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 F1 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 F1 holds
F1 . g = v . (g * f) ) & 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 F2 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 F2 holds
F2 . g = v . (g * f) ) implies F1 = F2 )
given Y1 being set such that Y1: for y being set holds
( y in Y1 iff ex h being Function st
( h in dom v & y in rng h ) ) and
A1: for a being set holds
( a in dom F1 iff ( a in Funcs N,Y1 & ex g being Function st
( a = g & g * f in dom v ) ) ) ; :: thesis: ( ex g being Function st
( g in dom F1 & not F1 . g = v . (g * f) ) or for Y being set holds
( ex y being set st
( ( y in Y implies ex h being Function st
( h in dom v & y in rng h ) ) implies ( ex h being Function st
( h in dom v & y in rng h ) & not y in Y ) ) or ex a being set st
( ( a in dom F2 implies ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) implies ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) & not a in dom F2 ) ) ) or ex g being Function st
( g in dom F2 & not F2 . g = v . (g * f) ) or F1 = F2 )
assume B1: for g being Function st g in dom F1 holds
F1 . g = v . (g * f) ; :: thesis: ( for Y being set holds
( ex y being set st
( ( y in Y implies ex h being Function st
( h in dom v & y in rng h ) ) implies ( ex h being Function st
( h in dom v & y in rng h ) & not y in Y ) ) or ex a being set st
( ( a in dom F2 implies ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) implies ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) & not a in dom F2 ) ) ) or ex g being Function st
( g in dom F2 & not F2 . g = v . (g * f) ) or F1 = F2 )
given Y2 being set such that Y2: for y being set holds
( y in Y2 iff ex h being Function st
( h in dom v & y in rng h ) ) and
A2: for a being set holds
( a in dom F2 iff ( a in Funcs N,Y2 & ex g being Function st
( a = g & g * f in dom v ) ) ) ; :: thesis: ( ex g being Function st
( g in dom F2 & not F2 . g = v . (g * f) ) or F1 = F2 )
assume B2: for g being Function st g in dom F2 holds
F2 . g = v . (g * f) ; :: thesis: F1 = F2

now

let a be set ; :: thesis: ( a in Y1 iff a in Y2 )
( a in Y1 iff ex h being Function st
( h in dom v & a in rng h ) ) by Y1;
hence ( a in Y1 iff a in Y2 ) by Y2; :: thesis: verum

end;

then Y3: Y1 = Y2 by TARSKI:2;

now

let a be set ; :: thesis: ( a in dom F1 iff a in dom F2 )
( a in dom F1 iff ( a in Funcs N,Y1 & ex g being Function st
( a = g & g * f in dom v ) ) ) by A1;
hence ( a in dom F1 iff a in dom F2 ) by A2, Y3; :: thesis: verum

end;

then A3: dom F1 = dom F2 by TARSKI:2;

now

let a be set ; :: thesis: ( a in dom F1 implies F1 . a = F2 . a )
assume A4: a in dom F1 ; :: thesis: F1 . a = F2 . a
then consider g being Function such that
A5: ( a = g & g * f in dom v ) by A1;
thus F1 . a = v . (g * f) by B1, A4, A5
.= F2 . a by B2, A3, A4, A5 ; :: thesis: verum

end;

hence F1 = F2 by A3, FUNCT_1:9; :: thesis: verum