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