set x = q `1 ;
set y = q `2 ;
set a = q `3 ;
let f1, f2 be BiFunction of (new_set2 A),L; :: thesis: ( ( for u, v being Element of A holds f1 . u,v = d . u,v ) & f1 . {A},{A} = Bottom L & f1 . {{A}},{{A}} = Bottom L & f1 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & f1 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( f1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f1 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & f1 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) & ( for u, v being Element of A holds f2 . u,v = d . u,v ) & f2 . {A},{A} = Bottom L & f2 . {{A}},{{A}} = Bottom L & f2 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & f2 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( f2 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f2 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f2 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & f2 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) implies f1 = f2 )
assume that
A20: for u, v being Element of A holds f1 . u,v = d . u,v and
A21: f1 . {A},{A} = Bottom L and
A22: f1 . {{A}},{{A}} = Bottom L and
A23: f1 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) and
A24: f1 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) and
A25: for u being Element of A holds
( f1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f1 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & f1 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) and
A26: for u, v being Element of A holds f2 . u,v = d . u,v and
A27: f2 . {A},{A} = Bottom L and
A28: f2 . {{A}},{{A}} = Bottom L and
A29: f2 . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) and
A30: f2 . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) and
A31: for u being Element of A holds
( f2 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & f2 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & f2 . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & f2 . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ; :: thesis: f1 = f2

now

let p, q be Element of new_set2 A; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂
A32: ( p in A or p in {{A},{{A}}} ) by XBOOLE_0:def 3;
A33: ( q in A or q in {{A},{{A}}} ) by XBOOLE_0:def 3;

per cases ( ( p in A & q in A ) or ( p in A & q = {A} ) or ( p in A & q = {{A}} ) or ( p = {A} & q in A ) or ( p = {A} & q = {A} ) or ( p = {A} & q = {{A}} ) or ( p = {{A}} & q in A ) or ( p = {{A}} & q = {A} ) or ( p = {{A}} & q = {{A}} ) ) by A32, A33, TARSKI:def 2;

suppose A34: ( p in A & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = d . p,q by A20
.= f2 . p,q by A26, A34 ;
:: thesis: verum

end;

suppose A35: ( p in A & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider p9 = p as Element of A ;
thus f1 . p,q = (d . p9,(q `1 )) "\/" (q `3 ) by A25, A35
.= f2 . p,q by A31, A35 ; :: thesis: verum

end;

suppose A36: ( p in A & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider p9 = p as Element of A ;
thus f1 . p,q = (d . p9,(q `2 )) "\/" (q `3 ) by A25, A36
.= f2 . p,q by A31, A36 ; :: thesis: verum

end;

suppose A37: ( p = {A} & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider q9 = q as Element of A ;
thus f1 . p,q = (d . q9,(q `1 )) "\/" (q `3 ) by A25, A37
.= f2 . p,q by A31, A37 ; :: thesis: verum

end;

suppose ( p = {A} & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A21, A27; :: thesis: verum

end;

suppose ( p = {A} & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A23, A29; :: thesis: verum

end;

suppose A38: ( p = {{A}} & q in A ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

then reconsider q9 = q as Element of A ;
thus f1 . p,q = (d . q9,(q `2 )) "\/" (q `3 ) by A25, A38
.= f2 . p,q by A31, A38 ; :: thesis: verum

end;

suppose ( p = {{A}} & q = {A} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A24, A30; :: thesis: verum

end;

suppose ( p = {{A}} & q = {{A}} ) ; :: thesis: f1 . b₁,b₂ = f2 . b₁,b₂

hence f1 . p,q = f2 . p,q by A22, A28; :: thesis: verum

end;

end;

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum