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