let L be non empty RelStr ; :: thesis: for N being non empty NetStr of L
for x being Element of L holds (x "/\" ) * N = x "/\" N
let N be non empty NetStr of L; :: thesis: for x being Element of L holds (x "/\" ) * N = x "/\" N
let x be Element of L; :: thesis: (x "/\" ) * N = x "/\" N
A1: RelStr(# the carrier of ((x "/\" ) * N),the InternalRel of ((x "/\" ) * N) #) = RelStr(# the carrier of N,the InternalRel of N #) by Def8
.= RelStr(# the carrier of (x "/\" N),the InternalRel of (x "/\" N) #) by WAYBEL_2:def 3 ;
set n = the mapping of N;
A2: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of (x "/\" N),the InternalRel of (x "/\" N) #) by WAYBEL_2:def 3;
then reconsider f2 = the mapping of (x "/\" N) as Function of the carrier of N,the carrier of L ;
A3: for c being Element of N holds ((x "/\" ) * the mapping of N) . c = f2 . c

proof

let c be Element of N; :: thesis: ((x "/\" ) * the mapping of N) . c = f2 . c
consider y being Element of L such that
A4: y = the mapping of N . c and
A5: f2 . c = x "/\" y by A2, WAYBEL_2:def 3;
thus ((x "/\" ) * the mapping of N) . c = (x "/\" ) . y by A4, FUNCT_2:21
.= f2 . c by A5, WAYBEL_1:def 18 ; :: thesis: verum

end;

the mapping of ((x "/\" ) * N) = (x "/\" ) * the mapping of N by Def8
.= the mapping of (x "/\" N) by A3, FUNCT_2:113 ;
hence (x "/\" ) * N = x "/\" N by A1; :: thesis: verum