let X1, X2, Y1, Y2 be set ; :: thesis: for f being Function st X1 c= X2 & Y1 c= Y2 holds
<:f,X1,Y1:> c= <:f,X2,Y2:>
let f be Function; :: thesis: ( X1 c= X2 & Y1 c= Y2 implies <:f,X1,Y1:> c= <:f,X2,Y2:> )
assume ( X1 c= X2 & Y1 c= Y2 ) ; :: thesis: <: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:> ; :: thesis: verum