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 Def2;
consider g2 being Function of A,B such that
A2: f = ~ [:g2,g2:] by Def3;
consider a being Element of A;
take b = g1 . a; :: thesis: f = [:A,A:] --> [b,b]
A3: dom f = [:A,A:] by FUNCT_2:def 1;

now

let z be set ; :: 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:9;
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 9;
then A8: [a1,a] in dom [:g2,g2:] by A5, ZFMISC_1:106;
A9: dom g2 = A by FUNCT_2:def 1;
[b,(g1 . a1)] = f . a,a1 by A1, A6, FUNCT_3:def 9
.= [:g2,g2:] . a1,a by A2, A8, FUNCT_4:def 2
.= [(g2 . a1),(g2 . a)] by A9, FUNCT_3:def 9 ;
then A10: g2 . a1 = b by ZFMISC_1:33;
A11: [a2,a] in dom [:g2,g2:] by A5, A7, ZFMISC_1:106;
[b,(g1 . a2)] = f . a,a2 by A1, A6, FUNCT_3:def 9
.= [:g2,g2:] . a2,a by A2, A11, FUNCT_4:def 2
.= [(g2 . a2),(g2 . a)] by A9, FUNCT_3:def 9 ;
then A12: g2 . a2 = b by ZFMISC_1:33;
A13: [a2,a1] in dom [:g2,g2:] by A5, A7, ZFMISC_1:106;
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 9 ; :: thesis: verum

end;

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