let x be object ; :: thesis: for M being non empty multMagma-yielding Function
for i being Element of dom M holds
( [i,x] in FreeAtoms M iff x in the carrier of (M . i) )
let M be non empty multMagma-yielding Function; :: thesis: for i being Element of dom M holds
( [i,x] in FreeAtoms M iff x in the carrier of (M . i) )
let i be Element of dom M; :: thesis: ( [i,x] in FreeAtoms M iff x in the carrier of (M . i) )
consider R being 1-sorted such that
A1: ( R = M . i & (Carrier M) . i = the carrier of R ) by PRALG_1:def 14;
thus ( [i,x] in FreeAtoms M implies x in the carrier of (M . i) ) by A1, Th7; :: thesis: ( x in the carrier of (M . i) implies [i,x] in FreeAtoms M )
assume x in the carrier of (M . i) ; :: thesis: [i,x] in FreeAtoms M
hence [i,x] in FreeAtoms M by A1, Th7; :: thesis: verum