let R, S, T be non empty RelStr ; :: thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj f,a) . b = (Proj f,b) . a
let f be Function of [:R,S:],T; :: thesis: for a being Element of R
for b being Element of S holds (Proj f,a) . b = (Proj f,b) . a
let a be Element of R; :: thesis: for b being Element of S holds (Proj f,a) . b = (Proj f,b) . a
let b be Element of S; :: thesis: (Proj f,a) . b = (Proj f,b) . a
(Proj f,a) . b = f . a,b by Th7
.= (Proj f,b) . a by Th8 ;
hence (Proj f,a) . b = (Proj f,b) . a ; :: thesis: verum