let X1, X2, Y1, Y2 be set ; for f being Function st X1 c= X2 & Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>
let f be Function; ( X1 c= X2 & Y1 c= Y2 implies <:f,X1,Y1:> c= <:f,X2,Y2:> )
assume
( X1 c= X2 & Y1 c= Y2 )
; <:f,X1,Y1:> c= <:f,X2,Y2:>
then
( <:f,X1,Y1:> c= <:f,X2,Y1:> & <:f,X2,Y1:> c= <:f,X2,Y2:> )
by Th28, Th29;
hence
<:f,X1,Y1:> c= <:f,X2,Y2:>
; verum