let A be non trivial set ; :: thesis: 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 Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let B be set ; :: thesis: for Bo1, Bo2 being Subset of B
for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let Bo1, Bo2 be Subset of B; :: thesis: for yo1 being Function of Bo1,A
for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let yo1 be Function of Bo1,A; :: thesis: for yo2 being Function of Bo2,A st Bo1 <> Bo2 & Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
let yo2 be Function of Bo2,A; :: thesis: ( Bo1 <> Bo2 & Bo2 c= Bo1 implies ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 ) )
assume that
A1: Bo1 <> Bo2 and
A2: Bo2 c= Bo1 ; :: thesis: ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 )
Bo2 c< Bo1 by A1, A2, XBOOLE_0:def 8;
then consider x0 being object such that
A3: x0 in Bo1 and
A4: not x0 in Bo2 by XBOOLE_0:6;
A5: x0 in dom yo1 by A3, FUNCT_2:def 1;
deffunc H1( object ) -> set = yo2 . $1;
defpred S1[ object ] means $1 in Bo2;
ex y0 being set st
( y0 in A & y0 <> yo1 . x0 )
proof
consider x, y being object such that
A6: x in A and
A7: y in A and
A8: x <> y by ZFMISC_1:def 10;
per cases ( yo1 . x0 = x or yo1 . x0 <> x ) ;
suppose A9: yo1 . x0 = x ; :: thesis: ex y0 being set st
( y0 in A & y0 <> yo1 . x0 )
take y ; :: thesis: ( y is set & y in A & y <> yo1 . x0 )
thus ( y is set & y in A & y <> yo1 . x0 ) by A7, A8, A9; :: thesis: verum
end;
suppose A10: yo1 . x0 <> x ; :: thesis: ex y0 being set st
( y0 in A & y0 <> yo1 . x0 )
take x ; :: thesis: ( x is set & x in A & x <> yo1 . x0 )
thus ( x is set & x in A & x <> yo1 . x0 ) by A6, A10; :: thesis: verum
end;
end;
end;
then consider y0 being set such that
A11: y0 in A and
A12: y0 <> yo1 . x0 ;
deffunc H2( object ) -> set = y0;
A13: 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 A11, FUNCT_2:5;
consider f being Function of B,A such that
A14: 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(A13);
A15: now :: thesis: for z being object st z in dom yo2 holds
yo2 . z = f . z
let z be object ; :: thesis: ( z in dom yo2 implies yo2 . z = f . z )
assume z in dom yo2 ; :: thesis: yo2 . z = f . z
then z in Bo2 ;
hence yo2 . z = f . z by A14; :: thesis: verum
end;
f . x0 <> yo1 . x0 by A3, A4, A12, A14;
then A16: f | Bo1 <> yo1 by A5, FUNCT_1:47;
dom yo2 = Bo2 by FUNCT_2:def 1
.= B /\ Bo2 by XBOOLE_1:28
.= (dom f) /\ Bo2 by FUNCT_2:def 1 ;
then f | Bo2 = yo2 by A15, FUNCT_1:46;
hence ex f being Function of B,A st
( f | Bo2 = yo2 & f | Bo1 <> yo1 ) by A16; :: thesis: verum