let A1, A2, B1, B2 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):]
let a be Element of [:Y1,Y2:]; :: according to FUNCT_2:def 8 :: thesis: ([:f,g:] | [:Y1,Y2:]) . a = [:(f | Y1),(g | Y2):] . a
consider a1 being Element of Y1, a2 being Element of Y2 such that
A1: a = [a1,a2] by DOMAIN_1:1;
A2: (g | Y2) . a2 = g . a2 by FUNCT_1:49;
A3: (f | Y1) . a1 = f . a1 by FUNCT_1:49;
thus [:(f | Y1),(g | Y2):] . a = [:(f | Y1),(g | Y2):] . (a1,a2) by A1
.= [(f . a1),(g . a2)] by A3, A2, Th75
.= [:f,g:] . (a1,a2) by Th75
.= ([:f,g:] | [:Y1,Y2:]) . a by A1, FUNCT_1:49 ; :: thesis: verum