let A, B be non empty set ; :: thesis: for f being Covariant Contravariant bifunction of A,B ex b being Element of B st f = [:A,A:] --> [b,b]
let f be Covariant Contravariant bifunction of A,B; :: thesis: ex b being Element of B st f = [:A,A:] --> [b,b]
consider g1 being Function of A,B such that
A1: f = [:g1,g1:] by Def1;
consider g2 being Function of A,B such that
A2: f = ~ [:g2,g2:] by Def2;
set a = the Element of A;
take b = g1 . the Element of A; :: thesis: f = [:A,A:] --> [b,b]
A3: dom f = [:A,A:] by FUNCT_2:def 1;

now :: thesis: for z being object st z in dom f holds
f . z = [b,b]

let z be object ; :: thesis: ( z in dom f implies f . z = [b,b] )
assume z in dom f ; :: thesis: f . z = [b,b]
then consider a1, a2 being Element of A such that
A4: z = [a1,a2] by DOMAIN_1:1;
A5: dom g2 = A by FUNCT_2:def 1;
A6: dom g1 = A by FUNCT_2:def 1;
A7: dom [:g2,g2:] = [:(dom g2),(dom g2):] by FUNCT_3:def 8;
then A8: [a1, the Element of A] in dom [:g2,g2:] by A5, ZFMISC_1:87;
A9: dom g2 = A by FUNCT_2:def 1;
[b,(g1 . a1)] = f . ( the Element of A,a1) by A1, A6, FUNCT_3:def 8
.= [:g2,g2:] . (a1, the Element of A) by A2, A8, FUNCT_4:def 2
.= [(g2 . a1),(g2 . the Element of A)] by A9, FUNCT_3:def 8 ;
then A10: g2 . a1 = b by XTUPLE_0:1;
A11: [a2, the Element of A] in dom [:g2,g2:] by A5, A7, ZFMISC_1:87;
[b,(g1 . a2)] = f . ( the Element of A,a2) by A1, A6, FUNCT_3:def 8
.= [:g2,g2:] . (a2, the Element of A) by A2, A11, FUNCT_4:def 2
.= [(g2 . a2),(g2 . the Element of A)] by A9, FUNCT_3:def 8 ;
then A12: g2 . a2 = b by XTUPLE_0:1;
A13: [a2,a1] in dom [:g2,g2:] by A5, A7, ZFMISC_1:87;
thus f . z = [:g1,g1:] . (a1,a2) by A1, A4
.= [:g2,g2:] . (a2,a1) by A1, A2, A13, FUNCT_4:def 2
.= [b,b] by A9, A10, A12, FUNCT_3:def 8 ; :: thesis: verum

end;

hence f = [:A,A:] --> [b,b] by A3, FUNCOP_1:11; :: thesis: verum