let B1, B2, A1, A2 be non empty set ; :: thesis: for f being Function of A1,B1
for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let f be Function of A1,B1; :: thesis: for g being Function of A2,B2
for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let g be Function of A2,B2; :: thesis: for Y1 being non empty Subset of A1
for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let Y1 be non empty Subset of A1; :: thesis: for Y2 being non empty Subset of A2 holds [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]
let Y2 be non empty Subset of A2; :: thesis: [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):]

now

let a be Element of [:Y1,Y2:]; :: thesis: [:(f | Y1),(g | Y2):] . a = ([:f,g:] | [:Y1,Y2:]) . a
consider a1 being Element of Y1, a2 being Element of Y2 such that
A1: a = [a1,a2] by DOMAIN_1:9;
A2: ( (f | Y1) . a1 = f . a1 & (g | Y2) . a2 = g . a2 ) by FUNCT_1:72;
thus [:(f | Y1),(g | Y2):] . a = [:(f | Y1),(g | Y2):] . a1,a2 by A1
.= [(f . a1),(g . a2)] by A2, FUNCT_3:96
.= [:f,g:] . a1,a2 by FUNCT_3:96
.= ([:f,g:] | [:Y1,Y2:]) . a by A1, FUNCT_1:72 ; :: thesis: verum

end;

hence [:f,g:] | [:Y1,Y2:] = [:(f | Y1),(g | Y2):] by FUNCT_2:113; :: thesis: verum