set x = q `1_4 ;
set y = q `2_4 ;
set a = q `3_4 ;
set b = q `4_4 ;
let f1, f2 be BiFunction of (new_set A),L; :: thesis:
assume that
A29: for u, v being Element of A holds f1 . (u,v) = d . (u,v) and
A30: f1 . ({A},{A}) = Bottom L and
A31: f1 . ({{A}},{{A}}) = Bottom L and
A32: f1 . ({{{A}}},{{{A}}}) = Bottom L and
A33: f1 . ({{A}},{{{A}}}) = q `3_4 and
A34: f1 . ({{{A}}},{{A}}) = q `3_4 and
A35: f1 . ({A},{{A}}) = q `4_4 and
A36: f1 . ({{A}},{A}) = q `4_4 and
A37: f1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) and
A38: f1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) and
A39: for u being Element of A holds
( f1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) and
A40: for u, v being Element of A holds f2 . (u,v) = d . (u,v) and
A41: f2 . ({A},{A}) = Bottom L and
A42: f2 . ({{A}},{{A}}) = Bottom L and
A43: f2 . ({{{A}}},{{{A}}}) = Bottom L and
A44: f2 . ({{A}},{{{A}}}) = q `3_4 and
A45: f2 . ({{{A}}},{{A}}) = q `3_4 and
A46: f2 . ({A},{{A}}) = q `4_4 and
A47: f2 . ({{A}},{A}) = q `4_4 and
A48: f2 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) and
A49: f2 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) and
A50: for u being Element of A holds
( f2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & f2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & f2 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f2 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & f2 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & f2 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ; :: thesis:

now :: thesis:

let p, q be Element of new_set A; :: thesis:
A51: ( p in A or p in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;
A52: ( q in A or q in {{A},{{A}},{{{A}}}} ) by XBOOLE_0:def 3;

per cases by A51, A52, ENUMSET1:def 1;

suppose A53: ( p in A & q in A ) ; :: thesis:

hence f1 . (p,q) = d . (p,q) by A29
.= f2 . (p,q) by A40, A53 ;
:: thesis:

end;

suppose A54: ( p in A & q = {A} ) ; :: thesis:

then reconsider p9 = p as Element of A ;
thus f1 . (p,q) = (d . (p9,(q `1_4))) "\/" (q `3_4) by A39, A54
.= f2 . (p,q) by A50, A54 ; :: thesis:

end;

suppose A55: ( p in A & q = {{A}} ) ; :: thesis:

then reconsider p9 = p as Element of A ;
thus f1 . (p,q) = ((d . (p9,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) by A39, A55
.= f2 . (p,q) by A50, A55 ; :: thesis:

end;

suppose A56: ( p in A & q = {{{A}}} ) ; :: thesis:

then reconsider p9 = p as Element of A ;
thus f1 . (p,q) = (d . (p9,(q `2_4))) "\/" (q `4_4) by A39, A56
.= f2 . (p,q) by A50, A56 ; :: thesis:

end;

suppose A57: ( p = {A} & q in A ) ; :: thesis:

then reconsider q9 = q as Element of A ;
thus f1 . (p,q) = (d . (q9,(q `1_4))) "\/" (q `3_4) by A39, A57
.= f2 . (p,q) by A50, A57 ; :: thesis:

end;

suppose ( p = {A} & q = {A} ) ; :: thesis:

hence f1 . (p,q) = f2 . (p,q) by A30, A41; :: thesis:

end;

suppose ( p = {A} & q = {{A}} ) ; :: thesis:

hence f1 . (p,q) = f2 . (p,q) by A35, A46; :: thesis:

end;

suppose ( p = {A} & q = {{{A}}} ) ; :: thesis:

hence f1 . (p,q) = f2 . (p,q) by A37, A48; :: thesis:

end;

suppose A58: ( p = {{A}} & q in A ) ; :: thesis:

then reconsider q9 = q as Element of A ;
thus f1 . (p,q) = ((d . (q9,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) by A39, A58
.= f2 . (p,q) by A50, A58 ; :: thesis:

end;