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 A1: for y being set holds

( y in Y1 iff ex h being Function st

( h in dom v & y in rng h ) ) and

A2: 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 A3: 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 A4: for y being set holds

( y in Y2 iff ex h being Function st

( h in dom v & y in rng h ) ) and

A5: 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 A8: for g being Function st g in dom F2 holds

F2 . g = v . (g * f) ; :: thesis: F1 = F2

( ( 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 A1: for y being set holds

( y in Y1 iff ex h being Function st

( h in dom v & y in rng h ) ) and

A2: 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 A3: 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 A4: for y being set holds

( y in Y2 iff ex h being Function st

( h in dom v & y in rng h ) ) and

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

now :: thesis: for a being object holds

( a in Y1 iff a in Y2 )

then A6:
Y1 = Y2
by TARSKI:2;( a in Y1 iff a in Y2 )

let a be object ; :: 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 A1;

hence ( a in Y1 iff a in Y2 ) by A4; :: thesis: verum

end;( a in Y1 iff ex h being Function st

( h in dom v & a in rng h ) ) by A1;

hence ( a in Y1 iff a in Y2 ) by A4; :: thesis: verum

now :: thesis: for a being object holds

( a in dom F1 iff a in dom F2 )

then A7:
dom F1 = dom F2
by TARSKI:2;( a in dom F1 iff a in dom F2 )

let a be object ; :: 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 A2;

hence ( a in dom F1 iff a in dom F2 ) by A5, A6; :: thesis: verum

end;( a in dom F1 iff ( a in Funcs (N,Y1) & ex g being Function st

( a = g & g * f in dom v ) ) ) by A2;

hence ( a in dom F1 iff a in dom F2 ) by A5, A6; :: thesis: verum

assume A8: for g being Function st g in dom F2 holds

F2 . g = v . (g * f) ; :: thesis: F1 = F2

now :: thesis: for a being object st a in dom F1 holds

F1 . a = F2 . a

hence
F1 = F2
by A7; :: thesis: verumF1 . a = F2 . a

let a be object ; :: thesis: ( a in dom F1 implies F1 . a = F2 . a )

assume A9: a in dom F1 ; :: thesis: F1 . a = F2 . a

then consider g being Function such that

A10: a = g and

g * f in dom v by A2;

thus F1 . a = v . (g * f) by A3, A9, A10

.= F2 . a by A8, A7, A9, A10 ; :: thesis: verum

end;assume A9: a in dom F1 ; :: thesis: F1 . a = F2 . a

then consider g being Function such that

A10: a = g and

g * f in dom v by A2;

thus F1 . a = v . (g * f) by A3, A9, A10

.= F2 . a by A8, A7, A9, A10 ; :: thesis: verum