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 not Bo2 c= Bo1 holds
ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 )
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 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; :: thesis: 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; :: thesis: 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; :: thesis: ( not Bo2 c= Bo1 implies ex f being Function of B,A st
( f | Bo1 = yo1 & f | Bo2 <> yo2 ) )
defpred S₁[ object ] means $1 in Bo1;
deffunc H₁( object ) -> set = yo1 . $1;
assume not Bo2 c= Bo1 ; :: thesis: 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 )

proof

consider x, y being object such that
A4: x in A and
A5: y in A and
A6: x <> y by ZFMISC_1:def 10;

per cases ( yo2 . x0 = x or yo2 . x0 <> x ) ;

suppose A7: yo2 . x0 = x ; :: thesis: ex y0 being set st
( y0 in A & y0 <> yo2 . x0 )

take y ; :: thesis: ( y is set & y in A & y <> yo2 . x0 )
thus ( y is set & y in A & y <> yo2 . x0 ) by A5, A6, A7; :: thesis: verum

end;

suppose A8: yo2 . x0 <> x ; :: thesis: ex y0 being set st
( y0 in A & y0 <> yo2 . x0 )

take x ; :: thesis: ( x is set & x in A & x <> yo2 . x0 )
thus ( x is set & x in A & x <> yo2 . x0 ) by A4, A8; :: thesis: verum

end;

end;

end;

then consider y0 being set such that
A9: y0 in A and
A10: y0 <> yo2 . x0 ;
deffunc H₂( object ) -> set = y0;
A11: for x being object st x in B holds
( ( S₁[x] implies H₁(x) in A ) & ( not S₁[x] implies H₂(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
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) from FUNCT_2:sch 5(A11);

A13: now :: thesis: for z being object st z in dom yo1 holds
yo1 . z = f . z

let z be object ; :: thesis: ( z in dom yo1 implies yo1 . z = f . z )
assume z in dom yo1 ; :: thesis: yo1 . z = f . z
then z in Bo1 ;
hence yo1 . z = f . z by A12; :: thesis: verum

end;

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; :: thesis: verum