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 )
now :: thesis: for a being object holds
( 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;
then A6: Y1 = Y2 by TARSKI:2;
now :: thesis: for a being object holds
( 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;
then A7: dom F1 = dom F2 by TARSKI:2;
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
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;
hence F1 = F2 by A7; :: thesis: verum