let R, S, T be non empty RelStr ; 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; 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; for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let b be Element of S; (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
; verum