let A be non trivial set ; for B being set
for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let B be set ; for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let Bo1, Bo2 be Subset of B; for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let yo1 be Function of Bo1,A; for yo2 being Function of Bo2,A st not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
let yo2 be Function of Bo2,A; ( not Bo2 c= Bo1 implies ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 ) )
defpred S1[ object ] means $1 in Bo1;
deffunc H1( object ) -> set = yo1 . $1;
assume
not Bo2 c= Bo1
; ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
then consider x0 being object such that
A1:
x0 in Bo2
and
A2:
not x0 in Bo1
;
A3:
x0 in dom yo2
by A1, FUNCT_2:def 1;
ex y0 being set st
( y0 in A & y0 <> yo2 . x0 )
then consider y0 being set such that
A9:
y0 in A
and
A10:
y0 <> yo2 . x0
;
deffunc H2( object ) -> set = y0;
A11:
for x being object st x in B holds
( ( S1[x] implies H1(x) in A ) & ( not S1[x] implies H2(x) in A ) )
by A9, FUNCT_2:5;
consider f being Function of B,A such that
A12:
for x being object st x in B holds
( ( S1[x] implies f . x = H1(x) ) & ( not S1[x] implies f . x = H2(x) ) )
from FUNCT_2:sch 5(A11);
f . x0 <> yo2 . x0
by A1, A2, A10, A12;
then A14:
f | Bo2 <> yo2
by A3, FUNCT_1:47;
dom yo1 =
Bo1
by FUNCT_2:def 1
.=
B /\ Bo1
by XBOOLE_1:28
.=
(dom f) /\ Bo1
by FUNCT_2:def 1
;
then
f | Bo1 = yo1
by A13, FUNCT_1:46;
hence
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
by A14; verum