let X be non empty set ; :: thesis: for F being BinOp of X

for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x)

let F be BinOp of X; :: thesis: for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x)

let x be Element of X; :: thesis: (F [:] ((id X),x)) . x = F . (x,x)

thus (F [:] ((id X),x)) . x = F . (((id X) . x),x) by Th48

.= F . (x,x) ; :: thesis: verum

for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x)

let F be BinOp of X; :: thesis: for x being Element of X holds (F [:] ((id X),x)) . x = F . (x,x)

let x be Element of X; :: thesis: (F [:] ((id X),x)) . x = F . (x,x)

thus (F [:] ((id X),x)) . x = F . (((id X) . x),x) by Th48

.= F . (x,x) ; :: thesis: verum